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

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

Proof of Theorem sylan9bb
StepHypRef Expression
1 sylan9bb.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21adantr 270 . 2  |-  ( (
ph  /\  th )  ->  ( ps  <->  ch )
)
3 sylan9bb.2 . . 3  |-  ( th 
->  ( ch  <->  ta )
)
43adantl 271 . 2  |-  ( (
ph  /\  th )  ->  ( ch  <->  ta )
)
52, 4bitrd 186 1  |-  ( (
ph  /\  th )  ->  ( 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:  sylan9bbr  451  bi2anan9  573  baibd  870  rbaibd  871  syl3an9b  1246  sbcomxyyz  1894  eqeq12  2100  eleq12  2152  sbhypf  2668  ceqsrex2v  2747  sseq12  3047  rexprg  3489  rextpg  3491  breq12  3842  opelopabg  4086  brabg  4087  opelopab2  4088  ralxpf  4570  rexxpf  4571  feq23  5134  f00  5186  fconstg  5191  f1oeq23  5231  f1o00  5272  f1oiso  5587  riota1a  5609  cbvmpt2x  5708  caovord  5798  caovord3  5800  genpelvl  7050  genpelvu  7051  nn0ind-raph  8833  elfz  9399  elfzp12  9480  shftfibg  10219  shftfib  10222  absdvdsb  10896  dvdsabsb  10897  dvdsabseq  10930
  Copyright terms: Public domain W3C validator