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

Theorem sylan9bb 455
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 272 . 2  |-  ( (
ph  /\  th )  ->  ( ps  <->  ch )
)
3 sylan9bb.2 . . 3  |-  ( th 
->  ( ch  <->  ta )
)
43adantl 273 . 2  |-  ( (
ph  /\  th )  ->  ( ch  <->  ta )
)
52, 4bitrd 187 1  |-  ( (
ph  /\  th )  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  sylan9bbr  456  bi2anan9  578  baibd  891  rbaibd  892  syl3an9b  1271  sbcomxyyz  1921  eqeq12  2128  eleq12  2180  sbhypf  2707  ceqsrex2v  2789  sseq12  3090  rexprg  3543  rextpg  3545  breq12  3902  opelopabg  4158  brabg  4159  opelopab2  4160  ralxpf  4653  rexxpf  4654  feq23  5226  f00  5282  fconstg  5287  f1oeq23  5327  f1o00  5368  f1oiso  5693  riota1a  5715  cbvmpox  5815  caovord  5908  caovord3  5910  rbropapd  6105  genpelvl  7284  genpelvu  7285  nn0ind-raph  9122  xnn0xadd0  9601  elfz  9747  elfzp12  9830  shftfibg  10543  shftfib  10546  absdvdsb  11418  dvdsabsb  11419  dvdsabseq  11452  tgss2  12154  lmbr  12288  xmetec  12512
  Copyright terms: Public domain W3C validator