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

Theorem syld3an3 1230
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 958 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
2 simp2 959 . 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 1185 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  syld3an1  1231  syld3an2  1232  brelrng  5102  resin  5700  moriotass  6582  omwordri  6818  oewordri  6838  gchaleph2  8552  gruf  8691  nnncan1  9342  lediv1  9880  lemuldiv  9894  supxrbnd  10912  bcval4  11603  ccatval3  11752  znnenlem  12816  dvdsmultr1  12889  dvdssub2  12892  ndvdsadd  12933  mrcsscl  13850  latnle  14519  latabs1  14521  latabs2  14522  latj4rot  14536  grpsubf  14873  grpinvsub  14876  grpnpcan  14885  subgsubcl  14960  divssub  15005  ghmsub  15019  odhash3  15215  dvrcl  15796  unitdvcl  15797  abvsubtri  15928  lspsntrim  16175  basgen2  17059  opnneiss  17187  restlp  17252  nmtri  18677  sincosq1lem  20410  logrec  20666  1pthon2v  21598  grpodivinv  21837  grpoinvdiv  21838  grpodivf  21839  gxsuc  21865  vcnegsubdi2  22059  vcsub4  22060  nvmval2  22129  nvsubadd  22141  nvaddsub4  22147  nvnncan  22149  nvpi  22160  nvmtri  22165  nvabs  22167  4ipval2  22209  ipval3  22210  isblo2  22289  blof  22291  nmblore  22292  nmlnoubi  22302  nmlnogt0  22303  shsubcl  22728  unopadj  23427  atexch  23889  atcvatlem  23893  ofldaddlt  24246  ind1  24421  inelsiga  24523  ghomf1olem  25110  btwnconn2  26041  ismtybnd  26530  mzprename  26820  pell14qrdivcl  26942  pwssplit4  27182  frlmsslss2  27236  lindsmm  27289  dvconstbi  27542  ibliccsinexp  27735  stoweidlem22  27761  lkrlsp2  29975  opcon2b  30069  opltcon2b  30078  oldmm3N  30091  oldmm4  30092  oldmj3  30095  oldmj4  30096  cmt2N  30122  cmt4N  30124  atleneN  30305  lplnri2N  30425  cdlema2N  30663  pmapojoinN  30839  ltrncnvatb  31009  trlval2  31034  trljat1  31037  cdleme18c  31164  cdleme19c  31176  cdlemeiota  31456  trlcocnv  31591  tendoplco2  31650  cdlemk6  31708  cdlemk7u  31741  cdlemk22  31764  cdlemk24-3  31774  cdlemkid2  31795  cdlemk11ta  31800  cdlemk11tc  31816  cdlemk47  31820  cdlemk52  31825  tendocnv  31893  dibelval1st1  32022  dibelval1st2N  32023  dihord2pre2  32098
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator