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

Theorem sylan9bbr 444
 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 443 . 2 ((𝜑𝜃) → (𝜓𝜏))
43ancoms 259 1 ((𝜃𝜑) → (𝜓𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  pm5.75  880  mpteq12f  3864  opelopabsb  4024  elreimasng  4718  fvelrnb  5248  fmptco  5357  fconstfvm  5406  f1oiso  5492  mpt2eq123  5591  dfoprab4f  5846  fmpt2x  5853  nnmword  6121  ltmpig  6494  qreccl  8673  0fz1  9010  zmodid2  9301  cbvrald  10293
 Copyright terms: Public domain W3C validator