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

Theorem syld3an2 1370
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an2.1 ((𝜑𝜒𝜃) → 𝜓)
syld3an2.2 ((𝜑𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syld3an2 ((𝜑𝜒𝜃) → 𝜏)

Proof of Theorem syld3an2
StepHypRef Expression
1 syld3an2.1 . . . 4 ((𝜑𝜒𝜃) → 𝜓)
213com23 1268 . . 3 ((𝜑𝜃𝜒) → 𝜓)
3 syld3an2.2 . . . 4 ((𝜑𝜓𝜃) → 𝜏)
433com23 1268 . . 3 ((𝜑𝜃𝜓) → 𝜏)
52, 4syld3an3 1368 . 2 ((𝜑𝜃𝜒) → 𝜏)
653com23 1268 1 ((𝜑𝜒𝜃) → 𝜏)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  nppcan2  10259  nnncan  10263  nnncan2  10265  ltdivmul  10845  ledivmul  10846  ltdiv23  10861  lediv23  10862  xrmaxlt  11958  xrltmin  11959  xrmaxle  11960  xrlemin  11961  swrdtrcfv  13382  dvdssub2  14950  dvdsgcdb  15189  lcmdvdsb  15253  vdwapun  15605  poslubdg  17073  ipodrsfi  17087  mulginvcom  17489  matinvgcell  20163  mdetrsca2  20332  mdetrlin2  20335  mdetunilem5  20344  decpmatmul  20499  islp3  20863  bddibl  23519  nvpi  27383  nvabs  27388  nmmulg  29806  subdivcomb2  31341  lineid  31853  oplecon1b  33989  opltcon1b  33993  oldmm2  34006  oldmj2  34010  cmt3N  34039  2llnneN  34196  cvrexchlem  34206  pmod2iN  34636  polcon2N  34706  paddatclN  34736  osumcllem3N  34745  ltrnval1  34921  cdleme48fv  35288  cdlemg33b  35496  trlcolem  35515  cdlemh  35606  cdlemi1  35607  cdlemi2  35608  cdlemi  35609  cdlemk4  35623  cdlemk19u1  35758  cdlemn3  35987  hgmapfval  36679  pell14qrgap  36940  stoweidlem22  39562  stoweidlem26  39566  sigarexp  40368  pfxtrcfv  40716  pfxco  40753  lindszr  41562
  Copyright terms: Public domain W3C validator