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

Theorem syld3an3 1410
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an3.1 ((𝜑𝜓𝜒) → 𝜃)
syld3an3.2 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syld3an3 ((𝜑𝜓𝜒) → 𝜏)

Proof of Theorem syld3an3
StepHypRef Expression
1 simp1 1137 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 1138 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1372 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  brelrng  5897  resin  6807  moriotass  7347  omwordri  8520  oewordri  8540  dif1en  9107  dif1enOLD  9109  sdomdomtrfi  9151  php3  9159  onomeneq  9175  preleqg  9556  gchaleph2  10613  gruf  10752  nnncan1  11442  lediv1  12025  lemuldiv  12040  suprfinzcl  12622  supxrbnd  13253  bcval4  14213  ccatval3  14473  ccatfv0  14477  ccatval1lsw  14478  ccatval21sw  14479  lswccatn0lsw  14485  pfxsuff1eqwrdeq  14593  pfxccatid  14635  cshwidxmodr  14698  2swrd2eqwrdeq  14848  dvdsmultr1  16183  dvdssub2  16188  ndvdsadd  16297  mrcsscl  17505  latnle  18367  latabs1  18369  latabs2  18370  latj4rot  18384  grpsubf  18831  grpinvsub  18834  grpnpcan  18844  mulginvcom  18906  mulginvinv  18907  subgsubcl  18944  qussub  18995  ghmsub  19021  odhash3  19363  srgcom4  19950  dvrcl  20120  unitdvcl  20121  abvsubtri  20308  lspsntrim  20574  frlmsslss2  21197  lindsmm  21250  ascldimul  21307  lply1binomsc  21694  smadiadetglem2  22037  m2cpm  22106  m2cpminvid  22118  pmatcollpwscmat  22156  mp2pm2mp  22176  cpmidgsum  22233  cpmadugsumfi  22242  basgen2  22355  opnneiss  22485  restlp  22550  nmtri  23998  csschl  24756  sincosq1lem  25870  logrec  26129  nosupbnd1lem2  27073  noinfbnd1lem2  27088  noetalem1  27105  grpodivinv  29520  grpoinvdiv  29521  grpodivf  29522  nvmval2  29627  nvaddsub4  29641  nvpi  29651  nvmtri  29655  nvabs  29656  4ipval2  29692  ipval3  29693  isblo2  29767  blof  29769  nmblore  29770  nmlnoubi  29780  nmlnogt0  29781  shsubcl  30204  unopadj  30903  atexch  31365  atcvatlem  31369  ogrpsublt  31978  ind1  32673  inelsiga  32791  inelros  32829  revpfxsfxrev  33766  mrsubcv  34161  mrsubvr  34162  btwnconn2  34733  ismtybnd  36312  lkrlsp2  37611  opcon2b  37705  opltcon2b  37714  oldmm3N  37727  oldmm4  37728  oldmj3  37731  oldmj4  37732  cmt2N  37758  cmt4N  37760  atleneN  37943  lplnri2N  38063  cdlema2N  38301  pmapojoinN  38477  ltrncnvatb  38647  trlval2  38672  trljat1  38675  cdleme18c  38802  cdleme19c  38814  cdlemeiota  39094  trlcocnv  39229  tendoplco2  39288  cdlemk6  39346  cdlemk7u  39379  cdlemk22  39402  cdlemk24-3  39412  cdlemkid2  39433  cdlemk11ta  39438  cdlemk11tc  39454  cdlemk47  39458  cdlemk52  39463  tendocnv  39530  dibelval1st1  39659  dibelval1st2N  39660  dihord2pre2  39735  mzprename  41115  pell14qrdivcl  41231  pwssplit4  41459  iocmbl  41590  relexpxpmin  42077  dvconstbi  42702  limsupgtlem  44104  dvbdfbdioolem1  44255  ibliccsinexp  44278  stoweidlem22  44349  fourierdlem42  44476  smfsuplem1  45138  divsub1dir  46684
  Copyright terms: Public domain W3C validator