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

Theorem syld3an3 1401
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 1128 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 1129 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1363 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  brelrng  5804  resin  6629  moriotass  7135  omwordri  8187  oewordri  8207  preleqg  9066  gchaleph2  10082  gruf  10221  nnncan1  10910  lediv1  11493  lemuldiv  11508  suprfinzcl  12085  supxrbnd  12709  bcval4  13655  ccatval3  13921  ccatfv0  13925  ccatval1lsw  13926  ccatval21sw  13927  lswccatn0lsw  13933  pfxsuff1eqwrdeq  14049  pfxccatid  14091  cshwidxmodr  14154  2swrd2eqwrdeq  14303  dvdsmultr1  15635  dvdssub2  15639  ndvdsadd  15749  mrcsscl  16879  latnle  17683  latabs1  17685  latabs2  17686  latj4rot  17700  grpsubf  18116  grpinvsub  18119  grpnpcan  18129  mulginvcom  18190  mulginvinv  18191  subgsubcl  18228  qussub  18278  ghmsub  18304  odhash3  18630  dvrcl  19365  unitdvcl  19366  abvsubtri  19535  lspsntrim  19799  ascldimul  20044  lply1binomsc  20403  frlmsslss2  20847  lindsmm  20900  smadiadetglem2  21209  m2cpm  21277  m2cpminvid  21289  pmatcollpwscmat  21327  mp2pm2mp  21347  cpmidgsum  21404  cpmadugsumfi  21413  basgen2  21525  opnneiss  21654  restlp  21719  nmtri  23162  csschl  23906  sincosq1lem  25010  logrec  25268  grpodivinv  28240  grpoinvdiv  28241  grpodivf  28242  nvmval2  28347  nvaddsub4  28361  nvpi  28371  nvmtri  28375  nvabs  28376  4ipval2  28412  ipval3  28413  isblo2  28487  blof  28489  nmblore  28490  nmlnoubi  28500  nmlnogt0  28501  shsubcl  28924  unopadj  29623  atexch  30085  atcvatlem  30089  ogrpsublt  30649  ind1  31175  inelsiga  31293  inelros  31331  revpfxsfxrev  32259  mrsubcv  32654  mrsubvr  32655  nosupbnd1lem2  33106  btwnconn2  33460  ismtybnd  34966  lkrlsp2  36119  opcon2b  36213  opltcon2b  36222  oldmm3N  36235  oldmm4  36236  oldmj3  36239  oldmj4  36240  cmt2N  36266  cmt4N  36268  atleneN  36450  lplnri2N  36570  cdlema2N  36808  pmapojoinN  36984  ltrncnvatb  37154  trlval2  37179  trljat1  37182  cdleme18c  37309  cdleme19c  37321  cdlemeiota  37601  trlcocnv  37736  tendoplco2  37795  cdlemk6  37853  cdlemk7u  37886  cdlemk22  37909  cdlemk24-3  37919  cdlemkid2  37940  cdlemk11ta  37945  cdlemk11tc  37961  cdlemk47  37965  cdlemk52  37970  tendocnv  38037  dibelval1st1  38166  dibelval1st2N  38167  dihord2pre2  38242  mzprename  39224  pell14qrdivcl  39340  pwssplit4  39567  iocmbl  39697  relexpxpmin  39940  dvconstbi  40543  limsupgtlem  41934  dvbdfbdioolem1  42089  ibliccsinexp  42112  stoweidlem22  42184  fourierdlem42  42311  smfsuplem1  42962  divsub1dir  44500
  Copyright terms: Public domain W3C validator