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

Theorem syld3an3 1411
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 1081 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 1082 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1366 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1054
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 197  df-an 385  df-3an 1056
This theorem is referenced by:  syld3an1  1412  syld3an2  1413  brelrng  5387  resin  6196  moriotass  6680  omwordri  7697  oewordri  7717  gchaleph2  9532  gruf  9671  nnncan1  10355  lediv1  10926  lemuldiv  10941  suprfinzcl  11530  supxrbnd  12196  bcval4  13134  ccatval3  13397  ccatfv0  13401  ccatval1lsw  13402  ccatval21sw  13403  lswccatn0lsw  13409  2swrd1eqwrdeq  13500  cshwidxmodr  13596  2swrd2eqwrdeq  13742  dvdsmultr1  15066  dvdssub2  15070  ndvdsadd  15181  mrcsscl  16327  latnle  17132  latabs1  17134  latabs2  17135  latj4rot  17149  grpsubf  17541  grpinvsub  17544  grpnpcan  17554  mulginvcom  17612  mulginvinv  17613  subgsubcl  17652  qussub  17701  ghmsub  17715  odhash3  18037  dvrcl  18732  unitdvcl  18733  abvsubtri  18883  lspsntrim  19146  lply1binomsc  19725  frlmsslss2  20162  lindsmm  20215  smadiadetglem2  20526  m2cpm  20594  m2cpminvid  20606  pmatcollpwscmat  20644  mp2pm2mp  20664  cpmidgsum  20721  cpmadugsumfi  20730  basgen2  20841  opnneiss  20970  restlp  21035  nmtri  22477  sincosq1lem  24294  logrec  24546  grpodivinv  27518  grpoinvdiv  27519  grpodivf  27520  nvmval2  27626  nvaddsub4  27640  nvpi  27650  nvmtri  27654  nvabs  27655  4ipval2  27691  ipval3  27692  isblo2  27766  blof  27768  nmblore  27769  nmlnoubi  27779  nmlnogt0  27780  shsubcl  28205  unopadj  28906  atexch  29368  atcvatlem  29372  ogrpsublt  29850  ind1  30207  inelsiga  30326  inelros  30364  mrsubcv  31533  mrsubvr  31534  nosupbnd1lem2  31980  btwnconn2  32334  ismtybnd  33736  lkrlsp2  34708  opcon2b  34802  opltcon2b  34811  oldmm3N  34824  oldmm4  34825  oldmj3  34828  oldmj4  34829  cmt2N  34855  cmt4N  34857  atleneN  35038  lplnri2N  35158  cdlema2N  35396  pmapojoinN  35572  ltrncnvatb  35742  trlval2  35768  trljat1  35771  cdleme18c  35898  cdleme19c  35910  cdlemeiota  36190  trlcocnv  36325  tendoplco2  36384  cdlemk6  36442  cdlemk7u  36475  cdlemk22  36498  cdlemk24-3  36508  cdlemkid2  36529  cdlemk11ta  36534  cdlemk11tc  36550  cdlemk47  36554  cdlemk52  36559  tendocnv  36627  dibelval1st1  36756  dibelval1st2N  36757  dihord2pre2  36832  mzprename  37629  pell14qrdivcl  37746  pwssplit4  37976  iocmbl  38115  relexpxpmin  38326  dvconstbi  38850  limsupgtlem  40327  dvbdfbdioolem1  40461  ibliccsinexp  40484  stoweidlem22  40557  fourierdlem42  40684  smfsuplem1  41338  pfxsuff1eqwrdeq  41732  pfxccatid  41755  divsub1dir  42632
  Copyright terms: Public domain W3C validator