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

Theorem sylan9bbr 451
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 450 . 2 ((𝜑𝜃) → (𝜓𝜏))
43ancoms 264 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.75  906  mpteq12f  3893  opelopabsb  4061  elreimasng  4765  fvelrnb  5315  fmptco  5427  fconstfvm  5476  f1oiso  5566  mpt2eq123  5665  dfoprab4f  5920  fmpt2x  5927  nnmword  6229  ltmpig  6842  qreccl  9059  0fz1  9391  zmodid2  9687  divgcdcoprm0  10958  cbvrald  11126
  Copyright terms: Public domain W3C validator