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

Theorem sylan9bbr 463
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 462 . 2 ((𝜑𝜃) → (𝜓𝜏))
43ancoms 268 1 ((𝜃𝜑) → (𝜓𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  pm5.75  962  mpteq12f  4084  opelopabsb  4261  elrelimasn  4995  fvelrnb  5564  fmptco  5683  fconstfvm  5735  f1oiso  5827  canth  5829  mpoeq123  5934  dfoprab4f  6194  fmpox  6201  nnmword  6519  elfi  6970  ltmpig  7338  mul0eqap  8627  qreccl  9642  0fz1  10045  zmodid2  10352  divgcdcoprm0  12101  cnptoprest  13742  txrest  13779  cbvrald  14543
  Copyright terms: Public domain W3C validator