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

Theorem sylan9bbr 463
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 462 . 2  |-  ( (
ph  /\  th )  ->  ( ps  <->  ta )
)
43ancoms 268 1  |-  ( ( th  /\  ph )  ->  ( ps  <->  ta )
)
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  4080  opelopabsb  4256  elrelimasn  4989  fvelrnb  5558  fmptco  5677  fconstfvm  5729  f1oiso  5820  canth  5822  mpoeq123  5927  dfoprab4f  6187  fmpox  6194  nnmword  6512  elfi  6963  ltmpig  7316  mul0eqap  8603  qreccl  9618  0fz1  10018  zmodid2  10325  divgcdcoprm0  12071  cnptoprest  13372  txrest  13409  cbvrald  14162
  Copyright terms: Public domain W3C validator