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  692  nfimt  1966  19.21tOLDOLD  2217  19.21t-1OLD  2353  ax13lem1  2389  ax13lem2  2437  axc11n  2447  axc11nOLD  2448  sbequi  2508  reuss2  4046  reupick  4050  elres  5589  ordtr2  5925  suc11  5988  funimass4  6405  fliftfun  6721  omlimcl  7823  nneob  7897  rankwflemb  8825  cflm  9260  domtriomlem  9452  grothomex  9839  sup3  11168  caubnd  14293  fbflim2  21978  ellimc3  23838  usgruspgrb  26271  usgredgsscusgredg  26561  3cyclfrgrrn1  27435  dfon2lem6  31994  opnrebl2  32618  axc11n11r  32975  stdpc5t  33116  wl-ax13lem1  33596  diaintclN  36845  dibintclN  36954  dihintcl  37131  pm11.71  39095  axc11next  39105
  Copyright terms: Public domain W3C validator