ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylan9bbr GIF version

Theorem sylan9bbr 456
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
Hypotheses
Ref Expression
sylan9bbr.1 (𝜑 → (𝜓𝜒))
sylan9bbr.2 (𝜃 → (𝜒𝜏))
Assertion
Ref Expression
sylan9bbr ((𝜃𝜑) → (𝜓𝜏))

Proof of Theorem sylan9bbr
StepHypRef Expression
1 sylan9bbr.1 . . 3 (𝜑 → (𝜓𝜒))
2 sylan9bbr.2 . . 3 (𝜃 → (𝜒𝜏))
31, 2sylan9bb 455 . 2 ((𝜑𝜃) → (𝜓𝜏))
43ancoms 266 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.75  927  mpteq12f  3966  opelopabsb  4140  elreimasng  4861  fvelrnb  5421  fmptco  5538  fconstfvm  5590  f1oiso  5679  mpoeq123  5782  dfoprab4f  6043  fmpox  6050  nnmword  6366  elfi  6809  ltmpig  7089  mul0eqap  8338  qreccl  9330  0fz1  9712  zmodid2  10012  divgcdcoprm0  11622  cnptoprest  12244  txrest  12281  cbvrald  12678
  Copyright terms: Public domain W3C validator