Theorem syld3an3 1422

Description: A syllogism inference.

Hypotheses

Ref	Expression
syld3an3.1	|- ((ph /\ ps /\ ch) -> th)
syld3an3.2	|- ((ph /\ ps /\ th) -> ta)

Assertion

Ref	Expression
syld3an3	|- ((ph /\ ps /\ ch) -> ta)

Proof of Theorem syld3an3

Step	Hyp	Ref	Expression
1		simp1 1148	. 2 |- ((ph /\ ps /\ ch) -> ph)
2		simp2 1149	. 2 |- ((ph /\ ps /\ ch) -> ps)
3		syld3an3.1	. 2 |- ((ph /\ ps /\ ch) -> th)
4		syld3an3.2	. 2 |- ((ph /\ ps /\ th) -> ta)
5	1, 2, 3, 4	syl111anc 1377	1 |- ((ph /\ ps /\ ch) -> ta)

Syntax hints:   -> wi 3   /\ w3a 1130

This theorem is referenced by:  syld3an1 1423  syld3an2 1424  brelrng 4343  resin 4782  omwordri 5454  oewordri 5473  fodomnumlem 6273  nnncan1 7206  lediv1 7468  lt2mul2divOLD 7490  lemuldiv 7493  supxrbnd 7752  geoisum1c 9023  znnenlem 9285  ndvdsadd 9441  1arithlem23 9553  latnle 9797  latabs1 9799  latabs2 9800  latj4rot 9814  opnneiss 10023  metcni2 10189  lmfexlem3 10252  grpdivinv 10389  grpinvdiv 10390  grpdivf 10391  gxsuc 10416  gacan 10481  vcnegsubdi2 10547  vcsub4 10548  nvsubadd 10628  nvaddsub4 10634  nvnncan 10636  nvpi 10647  nvmtri 10652  nvabs 10654  nvelbl2 10679  nvcni 10682  nvcni2 10683  nvcni3 10684  4ipval2 10718  ipval3 10719  isblo2 10806  blof 10808  nmblore 10809  nmlnoubi 10819  nmlnogt0 10820  sincosq1lem 11079  shsubcl 11715  unopadj 12470  atexch 12942  atcvatlem 12946  ghomf1olem 14621  grpdivzer 15736  multinvb 15786  mult2inv 15787  clsint 15875  dmse2 16055  2wsms 16061  flimfneicn 16092  fnctartar3 16357  opcon2b 17853  opltcon2b 17862  oldmm3 17875  oldmm4 17876  oldmj3 17879  oldmj4 17880  cmt2 17906  cmt4 17908  atlene 18094  lplnri2 18258  cdlema2 18496  pmapojoin 18653  ltrnlaut 18757  ltrncnv 18778  trlval4 18856  cdleme11c 18928  cdleme11d 18929  cdleme11e 18930  cdleme11j 18934  cdleme11l 18936  cdlemg1ci1 19256  cdlemg13a 19329  tendoplco2 19444

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

This theorem depends on definitions:  df-bi 232  df-an 435  df-3an 1132

Copyright terms: Public domain