Theorem 3syl 21

Description: Inference chaining two syllogisms.

Hypotheses

Ref	Expression
3syl.1	|- (ph -> ps)
3syl.2	|- (ps -> ch)
3syl.3	|- (ch -> th)

Assertion

Ref	Expression
3syl	|- (ph -> th)

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 |- (ph -> ps)
2		3syl.2	. . 3 |- (ps -> ch)
3	1, 2	syl 12	. 2 |- (ph -> ch)
4		3syl.3	. 2 |- (ch -> th)
5	3, 4	syl 12	1 |- (ph -> th)

Syntax hints:   -> wi 2

This theorem is referenced by:  19.9d 720  hbs1f 874  hbsb4 905  ddelimdf 909  sbcom 916  mo 1020  eupickb 1056  2eu2 1068  rgen2 1248  npss0 1731  opthwiener 1914  iununi 2037  onin 2229  ssorduni 2249  onelsst 2255  onssneli 2349  onuninsuc 2356  limsuclem 2360  limsuc 2361  dmsnop 2547  dmexg 2551  rnexg 2569  cnvexg 2669  coexg 2671  fununi 2705  resfunexg 2717  fn0 2739  fssxp 2761  foima 2790  fornex 2793  f1imacnv 2814  f1ococnv2 2817  f1dmex 2819  fvres 2840  cbvfo 2923  isomin 2937  isoini 2938  isofrlem 2939  isowe 2941  canth 2945  tfrlem10 2958  tfrlem11 2959  tfrlem13 2961  tz7.44-2 2967  tz7.44-3 2968  rdglem2 2976  omv 3120  oev 3122  oe1m 3147  oaord 3149  oawordeulem 3156  oalimcl 3162  oen0 3165  nnacom 3175  nndi 3180  nnmordi 3188  nnmord 3189  eceqopreq 3249  mapex 3261  map0 3268  f1imaen 3327  en1 3331  xpdom1 3346  xpdom3 3347  sbthlem1 3349  sbthlem2 3350  sbth 3359  mapenlem2 3385  phplem5 3407  php3 3411  php4 3412  0sdom1dom 3420  ssnn 3429  unblem1 3431  unfilem1 3438  fiint 3445  inf3lem7 3470  tz9.12lem3 3505  r1val3 3523  scott0 3542  aceq5lem4 3561  ac6lem 3575  numthlem 3598  numth 3599  zornlem2 3604  zornlem7 3609  fodom 3613  oncard 3636  sucdom 3648  unxpdomlem 3649  sucxpdom 3652  cardlim 3657  ondomon 3662  carduni 3664  cardaleph 3690  iscard3 3693  cdadom2 3728  nd3 3734  mulidpi 3808  ltsopi 3810  mulcanpi 3821  enqeceq 3841  addclpq 3852  mulclpq 3854  1qec 3862  ltapq 3870  halfpq 3876  prnmadd 3894  addclprlem2 3913  1idpr 3927  prlem934a 3931  prlem934 3933  ltaddpr 3934  ltexprlem3 3938  ltexprlem4 3939  ltexprlem6 3941  prlem936a 3947  prlem936 3949  reclem1pr 3950  suplem2pr 3956  enreceq 3971  addclsr 3986  mulclsr 3987  suppsr 4016  suppsr2 4017  supsrlem2 4020  axrecex 4079  nnleltp1t 4448  nn0ltp1let 4556  uzwo3lem2 4615  zbtwnre 4619  flgzt 4626  flidt 4627  zqt 4632  qbtwnre 4650  om2uzlt 4654  om2uzf1o 4656  uzrdgsuc 4659  seqval 4665  discrlem2 4714  discrlem3 4715  nnesq 4720  sqrlem12 4742  climunii 4883  znnen 4930  infxpidmlem11 4943  infdif 4948  infmap1 4950  infmap2 4953  alephexp2 4956  shaddclt 5123  shmulclt 5124  hlimunii 5143  occllem6 5185  projlem1 5193  projlem8 5200  projlem10 5202  projlem12 5204  projlem13 5205  projlem15 5207  projlem22 5214  projlem24 5216  projlem25 5217  projlem26 5218  pjthlem2 5226  pjthlem7 5231  pjthlem8 5232  dfch2 5254  ococint 5298  spanssoc 5320  spansncht 5465  osumlem3 5532  osumlem5 5534  5oalem5 5548  pjocin 5583  pjclem4 5653  pj2cocl 5657  pj3s 5659  stge0t 5673  stle1t 5674  strlem1 5691  strlem3a 5693  strlem5 5696  strlem6 5697  h1dat 5747  atom1d 5750  mdsymlem1 5776  mdsymlem3 5778  mdsym 5784  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6

metamath.org