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

Theorem sylan9bbr 436
 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 435 . 2 ((𝜑𝜃) → (𝜓𝜏))
43ancoms 255 1 ((𝜃𝜑) → (𝜓𝜏))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  pm5.75  869  mpteq12f  3837  opelopabsb  3997  elreimasng  4691  fvelrnb  5221  fmptco  5330  fconstfvm  5379  f1oiso  5465  mpt2eq123  5564  dfoprab4f  5819  fmpt2x  5826  nnmword  6091  ltmpig  6437  qreccl  8576  0fz1  8909  cbvrald  9927
 Copyright terms: Public domain W3C validator