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  965  mpteq12f  4124  opelopabsb  4306  elrelimasn  5048  fvelrnb  5626  fmptco  5746  fconstfvm  5802  f1oiso  5895  canth  5897  mpoeq123  6004  elovmporab  6146  elovmporab1w  6147  dfoprab4f  6279  fmpox  6286  nnmword  6604  elfi  7073  ltmpig  7452  mul0eqap  8743  qreccl  9763  0fz1  10167  zmodid2  10497  divgcdcoprm0  12423  cnptoprest  14711  txrest  14748  cbvrald  15724
  Copyright terms: Public domain W3C validator