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

Theorem syld3an3 1406
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 1133 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 1134 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1368 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  brelrng  5779  resin  6615  moriotass  7129  omwordri  8185  oewordri  8205  preleqg  9066  gchaleph2  10087  gruf  10226  nnncan1  10915  lediv1  11498  lemuldiv  11513  suprfinzcl  12089  supxrbnd  12713  bcval4  13667  ccatval3  13928  ccatfv0  13932  ccatval1lsw  13933  ccatval21sw  13934  lswccatn0lsw  13940  pfxsuff1eqwrdeq  14056  pfxccatid  14098  cshwidxmodr  14161  2swrd2eqwrdeq  14310  dvdsmultr1  15642  dvdssub2  15646  ndvdsadd  15754  mrcsscl  16886  latnle  17690  latabs1  17692  latabs2  17693  latj4rot  17707  grpsubf  18173  grpinvsub  18176  grpnpcan  18186  mulginvcom  18247  mulginvinv  18248  subgsubcl  18285  qussub  18335  ghmsub  18361  odhash3  18696  dvrcl  19435  unitdvcl  19436  abvsubtri  19602  lspsntrim  19866  frlmsslss2  20467  lindsmm  20520  ascldimul  20576  lply1binomsc  20939  smadiadetglem2  21280  m2cpm  21349  m2cpminvid  21361  pmatcollpwscmat  21399  mp2pm2mp  21419  cpmidgsum  21476  cpmadugsumfi  21485  basgen2  21597  opnneiss  21726  restlp  21791  nmtri  23235  csschl  23983  sincosq1lem  25093  logrec  25352  grpodivinv  28322  grpoinvdiv  28323  grpodivf  28324  nvmval2  28429  nvaddsub4  28443  nvpi  28453  nvmtri  28457  nvabs  28458  4ipval2  28494  ipval3  28495  isblo2  28569  blof  28571  nmblore  28572  nmlnoubi  28582  nmlnogt0  28583  shsubcl  29006  unopadj  29705  atexch  30167  atcvatlem  30171  ogrpsublt  30775  ind1  31384  inelsiga  31502  inelros  31540  revpfxsfxrev  32470  mrsubcv  32865  mrsubvr  32866  nosupbnd1lem2  33317  btwnconn2  33671  ismtybnd  35238  lkrlsp2  36392  opcon2b  36486  opltcon2b  36495  oldmm3N  36508  oldmm4  36509  oldmj3  36512  oldmj4  36513  cmt2N  36539  cmt4N  36541  atleneN  36723  lplnri2N  36843  cdlema2N  37081  pmapojoinN  37257  ltrncnvatb  37427  trlval2  37452  trljat1  37455  cdleme18c  37582  cdleme19c  37594  cdlemeiota  37874  trlcocnv  38009  tendoplco2  38068  cdlemk6  38126  cdlemk7u  38159  cdlemk22  38182  cdlemk24-3  38192  cdlemkid2  38213  cdlemk11ta  38218  cdlemk11tc  38234  cdlemk47  38238  cdlemk52  38243  tendocnv  38310  dibelval1st1  38439  dibelval1st2N  38440  dihord2pre2  38515  mzprename  39677  pell14qrdivcl  39793  pwssplit4  40020  iocmbl  40150  relexpxpmin  40405  dvconstbi  41025  limsupgtlem  42406  dvbdfbdioolem1  42557  ibliccsinexp  42580  stoweidlem22  42651  fourierdlem42  42778  smfsuplem1  43429  divsub1dir  44913
  Copyright terms: Public domain W3C validator