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

Theorem syld3an3 1515
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 1130 . 2 ((𝜑𝜓𝜒) → 𝜑)
2 simp2 1131 . 2 ((𝜑𝜓𝜒) → 𝜓)
3 syld3an3.1 . 2 ((𝜑𝜓𝜒) → 𝜃)
4 syld3an3.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1476 1 ((𝜑𝜓𝜒) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  syld3an1OLD  1517  syld3an2OLD  1519  brelrng  5493  resin  6299  moriotass  6783  omwordri  7806  oewordri  7826  preleqg  8674  gchaleph2  9696  gruf  9835  nnncan1  10519  lediv1  11090  lemuldiv  11105  suprfinzcl  11694  supxrbnd  12363  bcval4  13298  ccatval3  13561  ccatfv0  13565  ccatval1lsw  13566  ccatval21sw  13567  lswccatn0lsw  13573  2swrd1eqwrdeq  13663  cshwidxmodr  13759  2swrd2eqwrdeq  13906  dvdsmultr1  15228  dvdssub2  15232  ndvdsadd  15342  mrcsscl  16488  latnle  17293  latabs1  17295  latabs2  17296  latj4rot  17310  grpsubf  17702  grpinvsub  17705  grpnpcan  17715  mulginvcom  17773  mulginvinv  17774  subgsubcl  17813  qussub  17862  ghmsub  17876  odhash3  18198  dvrcl  18894  unitdvcl  18895  abvsubtri  19045  lspsntrim  19311  lply1binomsc  19892  frlmsslss2  20331  lindsmm  20384  smadiadetglem2  20697  m2cpm  20766  m2cpminvid  20778  pmatcollpwscmat  20816  mp2pm2mp  20836  cpmidgsum  20893  cpmadugsumfi  20902  basgen2  21014  opnneiss  21143  restlp  21208  nmtri  22650  sincosq1lem  24470  logrec  24722  grpodivinv  27730  grpoinvdiv  27731  grpodivf  27732  nvmval2  27838  nvaddsub4  27852  nvpi  27862  nvmtri  27866  nvabs  27867  4ipval2  27903  ipval3  27904  isblo2  27978  blof  27980  nmblore  27981  nmlnoubi  27991  nmlnogt0  27992  shsubcl  28417  unopadj  29118  atexch  29580  atcvatlem  29584  ogrpsublt  30062  ind1  30419  inelsiga  30538  inelros  30576  mrsubcv  31745  mrsubvr  31746  nosupbnd1lem2  32192  btwnconn2  32546  ismtybnd  33938  lkrlsp2  34912  opcon2b  35006  opltcon2b  35015  oldmm3N  35028  oldmm4  35029  oldmj3  35032  oldmj4  35033  cmt2N  35059  cmt4N  35061  atleneN  35242  lplnri2N  35362  cdlema2N  35600  pmapojoinN  35776  ltrncnvatb  35946  trlval2  35972  trljat1  35975  cdleme18c  36102  cdleme19c  36114  cdlemeiota  36394  trlcocnv  36529  tendoplco2  36588  cdlemk6  36646  cdlemk7u  36679  cdlemk22  36702  cdlemk24-3  36712  cdlemkid2  36733  cdlemk11ta  36738  cdlemk11tc  36754  cdlemk47  36758  cdlemk52  36763  tendocnv  36831  dibelval1st1  36960  dibelval1st2N  36961  dihord2pre2  37036  mzprename  37838  pell14qrdivcl  37955  pwssplit4  38185  iocmbl  38324  relexpxpmin  38535  dvconstbi  39059  limsupgtlem  40527  dvbdfbdioolem1  40661  ibliccsinexp  40684  stoweidlem22  40756  fourierdlem42  40883  smfsuplem1  41537  pfxsuff1eqwrdeq  41935  pfxccatid  41958  divsub1dir  42835
  Copyright terms: Public domain W3C validator