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

Theorem sylan9bbr 451
Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)
Hypotheses
Ref Expression
sylan9bbr.1  |-  ( ph  ->  ( ps  <->  ch )
)
sylan9bbr.2  |-  ( th 
->  ( ch  <->  ta )
)
Assertion
Ref Expression
sylan9bbr  |-  ( ( th  /\  ph )  ->  ( ps  <->  ta )
)

Proof of Theorem sylan9bbr
StepHypRef Expression
1 sylan9bbr.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 sylan9bbr.2 . . 3  |-  ( th 
->  ( ch  <->  ta )
)
31, 2sylan9bb 450 . 2  |-  ( (
ph  /\  th )  ->  ( ps  <->  ta )
)
43ancoms 264 1  |-  ( ( th  /\  ph )  ->  ( ps  <->  ta )
)
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  904  mpteq12f  3866  opelopabsb  4023  elreimasng  4721  fvelrnb  5253  fmptco  5362  fconstfvm  5411  f1oiso  5496  mpt2eq123  5595  dfoprab4f  5850  fmpt2x  5857  nnmword  6157  ltmpig  6591  qreccl  8808  0fz1  9140  zmodid2  9434  divgcdcoprm0  10627  cbvrald  10749
  Copyright terms: Public domain W3C validator