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

Theorem syl9 77
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
Hypotheses
Ref Expression
syl9.1 (𝜑 → (𝜓𝜒))
syl9.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
syl9 (𝜑 → (𝜃 → (𝜓𝜏)))

Proof of Theorem syl9
StepHypRef Expression
1 syl9.1 . 2 (𝜑 → (𝜓𝜒))
2 syl9.2 . . 3 (𝜃 → (𝜒𝜏))
32a1i 11 . 2 (𝜑 → (𝜃 → (𝜒𝜏)))
41, 3syl5d 73 1 (𝜑 → (𝜃 → (𝜓𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl9r  78  com23  86  sylan9  510  19.38a  1836  ax13lem1  2388  ax13lem2  2390  axc11n  2444  sbequiOLD  2530  sbequiALT  2592  reuss2  4282  reupick  4286  elinxp  5889  ordtr2  6234  suc11  6293  funimass4  6729  fliftfun  7064  omlimcl  8203  nneob  8278  rankwflemb  9221  cflm  9671  domtriomlem  9863  grothomex  10250  sup3  11597  caubnd  14717  fbflim2  22584  ellimc3  24476  usgruspgrb  26965  usgredgsscusgredg  27240  3cyclfrgrrn1  28063  dfon2lem6  33033  opnrebl2  33669  bj-nfimt  33971  axc11n11r  34017  bj-nnf-alrim  34084  stdpc5t  34150  wl-ax13lem1  34745  diaintclN  38193  dibintclN  38302  dihintcl  38479  pm11.71  40729  axc11next  40738  rrx2plord2  44710
  Copyright terms: Public domain W3C validator