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  571  baibd  866  rbaibd  867  syl3an9b  1242  sbcomxyyz  1888  eqeq12  2094  eleq12  2144  sbhypf  2649  ceqsrex2v  2728  sseq12  3023  rexprg  3452  rextpg  3454  breq12  3798  opelopabg  4031  brabg  4032  opelopab2  4033  ralxpf  4510  rexxpf  4511  feq23  5064  f00  5112  fconstg  5114  f1oeq23  5151  f1o00  5192  f1oiso  5496  riota1a  5518  cbvmpt2x  5613  caovord  5703  caovord3  5705  genpelvl  6764  genpelvu  6765  nn0ind-raph  8545  elfz  9111  elfzp12  9192  shftfibg  9846  shftfib  9849  absdvdsb  10358  dvdsabsb  10359  dvdsabseq  10392
  Copyright terms: Public domain W3C validator