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  508  19.38a  1831  ax13lem1  2383  ax13lem2  2385  axc11n  2440  sbequiOLD  2527  sbequiALT  2589  reuss2  4280  reupick  4284  elinxp  5883  ordtr2  6228  suc11  6287  funimass4  6723  fliftfun  7054  omlimcl  8193  nneob  8268  rankwflemb  9210  cflm  9660  domtriomlem  9852  grothomex  10239  sup3  11586  caubnd  14706  fbflim2  22513  ellimc3  24404  usgruspgrb  26893  usgredgsscusgredg  27168  3cyclfrgrrn1  27991  dfon2lem6  32930  opnrebl2  33566  bj-nfimt  33868  axc11n11r  33914  bj-nnf-alrim  33981  stdpc5t  34047  wl-ax13lem1  34628  diaintclN  38074  dibintclN  38183  dihintcl  38360  pm11.71  40606  axc11next  40615  rrx2plord2  44637
  Copyright terms: Public domain W3C validator