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

Theorem syld3an3 1521
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 1159 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 1160 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1483 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  syld3an1OLD  1523  syld3an2OLD  1525  brelrng  5570  resin  6384  moriotass  6874  omwordri  7899  oewordri  7919  preleqg  8767  gchaleph2  9789  gruf  9928  nnncan1  10612  lediv1  11183  lemuldiv  11198  suprfinzcl  11778  supxrbnd  12396  bcval4  13334  ccatval3  13596  ccatfv0  13600  ccatval1lsw  13601  ccatval21sw  13602  lswccatn0lsw  13608  2swrd1eqwrdeq  13698  cshwidxmodr  13794  2swrd2eqwrdeq  13941  dvdsmultr1  15262  dvdssub2  15266  ndvdsadd  15373  mrcsscl  16505  latnle  17310  latabs1  17312  latabs2  17313  latj4rot  17327  grpsubf  17719  grpinvsub  17722  grpnpcan  17732  mulginvcom  17789  mulginvinv  17790  subgsubcl  17827  qussub  17876  ghmsub  17890  odhash3  18212  dvrcl  18908  unitdvcl  18909  abvsubtri  19059  lspsntrim  19325  lply1binomsc  19905  frlmsslss2  20345  lindsmm  20398  smadiadetglem2  20711  m2cpm  20780  m2cpminvid  20792  pmatcollpwscmat  20830  mp2pm2mp  20850  cpmidgsum  20907  cpmadugsumfi  20916  basgen2  21028  opnneiss  21157  restlp  21222  nmtri  22664  sincosq1lem  24487  logrec  24738  grpodivinv  27742  grpoinvdiv  27743  grpodivf  27744  nvmval2  27849  nvaddsub4  27863  nvpi  27873  nvmtri  27877  nvabs  27878  4ipval2  27914  ipval3  27915  isblo2  27989  blof  27991  nmblore  27992  nmlnoubi  28002  nmlnogt0  28003  shsubcl  28428  unopadj  29129  atexch  29591  atcvatlem  29595  ogrpsublt  30070  ind1  30427  inelsiga  30546  inelros  30584  mrsubcv  31752  mrsubvr  31753  nosupbnd1lem2  32198  btwnconn2  32552  ismtybnd  33936  lkrlsp2  34902  opcon2b  34996  opltcon2b  35005  oldmm3N  35018  oldmm4  35019  oldmj3  35022  oldmj4  35023  cmt2N  35049  cmt4N  35051  atleneN  35233  lplnri2N  35353  cdlema2N  35591  pmapojoinN  35767  ltrncnvatb  35937  trlval2  35962  trljat1  35965  cdleme18c  36092  cdleme19c  36104  cdlemeiota  36384  trlcocnv  36519  tendoplco2  36578  cdlemk6  36636  cdlemk7u  36669  cdlemk22  36692  cdlemk24-3  36702  cdlemkid2  36723  cdlemk11ta  36728  cdlemk11tc  36744  cdlemk47  36748  cdlemk52  36753  tendocnv  36820  dibelval1st1  36949  dibelval1st2N  36950  dihord2pre2  37025  mzprename  37832  pell14qrdivcl  37949  pwssplit4  38178  iocmbl  38316  relexpxpmin  38527  dvconstbi  39051  limsupgtlem  40507  dvbdfbdioolem1  40641  ibliccsinexp  40664  stoweidlem22  40736  fourierdlem42  40863  smfsuplem1  41517  pfxsuff1eqwrdeq  42000  pfxccatid  42023  divsub1dir  42893
  Copyright terms: Public domain W3C validator