MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld3an3 Unicode version

Theorem syld3an3 1229
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
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
StepHypRef Expression
1 simp1 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
2 simp2 958 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
3 syld3an3.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
4 syld3an3.2 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
51, 2, 3, 4syl3anc 1184 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syld3an1  1230  syld3an2  1231  brelrng  5058  resin  5656  moriotass  6538  omwordri  6774  oewordri  6794  gchaleph2  8507  gruf  8642  nnncan1  9293  lediv1  9831  lemuldiv  9845  supxrbnd  10863  bcval4  11553  ccatval3  11702  znnenlem  12766  dvdsmultr1  12839  dvdssub2  12842  ndvdsadd  12883  mrcsscl  13800  latnle  14469  latabs1  14471  latabs2  14472  latj4rot  14486  grpsubf  14823  grpinvsub  14826  grpnpcan  14835  subgsubcl  14910  divssub  14955  ghmsub  14969  odhash3  15165  dvrcl  15746  unitdvcl  15747  abvsubtri  15878  lspsntrim  16125  basgen2  17009  opnneiss  17137  restlp  17201  nmtri  18625  sincosq1lem  20358  logrec  20614  1pthon2v  21546  grpodivinv  21785  grpoinvdiv  21786  grpodivf  21787  gxsuc  21813  vcnegsubdi2  22007  vcsub4  22008  nvmval2  22077  nvsubadd  22089  nvaddsub4  22095  nvnncan  22097  nvpi  22108  nvmtri  22113  nvabs  22115  4ipval2  22157  ipval3  22158  isblo2  22237  blof  22239  nmblore  22240  nmlnoubi  22250  nmlnogt0  22251  shsubcl  22676  unopadj  23375  atexch  23837  atcvatlem  23841  ofldaddlt  24194  ind1  24369  inelsiga  24471  ghomf1olem  25058  btwnconn2  25940  ismtybnd  26406  mzprename  26696  pell14qrdivcl  26818  pwssplit4  27059  frlmsslss2  27113  lindsmm  27166  dvconstbi  27419  ibliccsinexp  27612  stoweidlem22  27638  lkrlsp2  29586  opcon2b  29680  opltcon2b  29689  oldmm3N  29702  oldmm4  29703  oldmj3  29706  oldmj4  29707  cmt2N  29733  cmt4N  29735  atleneN  29916  lplnri2N  30036  cdlema2N  30274  pmapojoinN  30450  ltrncnvatb  30620  trlval2  30645  trljat1  30648  cdleme18c  30775  cdleme19c  30787  cdlemeiota  31067  trlcocnv  31202  tendoplco2  31261  cdlemk6  31319  cdlemk7u  31352  cdlemk22  31375  cdlemk24-3  31385  cdlemkid2  31406  cdlemk11ta  31411  cdlemk11tc  31427  cdlemk47  31431  cdlemk52  31436  tendocnv  31504  dibelval1st1  31633  dibelval1st2N  31634  dihord2pre2  31709
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator