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

Theorem syl9r 78
Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)
Hypotheses
Ref Expression
syl9r.1 (𝜑 → (𝜓𝜒))
syl9r.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
syl9r (𝜃 → (𝜑 → (𝜓𝜏)))

Proof of Theorem syl9r
StepHypRef Expression
1 syl9r.1 . . 3 (𝜑 → (𝜓𝜒))
2 syl9r.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2syl9 77 . 2 (𝜑 → (𝜃 → (𝜓𝜏)))
43com12 32 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:  sylan9r  505  19.38b  1937  ax12v2  2215  fununi  6175  dfimafn  6470  funimass3  6559  isomin  6815  oneqmin  7239  tz7.48lem  7775  fisupg  8450  fiinfg  8647  trcl  8854  coflim  9371  coftr  9383  axdc3lem2  9561  konigthlem  9678  indpi  10017  nnsub  11357  2ndc1stc  21583  kgencn2  21689  tx1stc  21782  filuni  22017  fclscf  22157  alexsubALTlem2  22180  alexsubALTlem3  22181  alexsubALT  22183  lpni  27860  dfimafnf  29955  dfon2lem6  32205  nodenselem8  32354  bj-exlalrim  33109  finixpnum  33883  heiborlem4  34100  lncvrelatN  35802  imbi13  39506  dfaimafn  42019  sgoldbeven3prm  42453
  Copyright terms: Public domain W3C validator