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

Theorem bibi12d 233
Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
imbi12d.1  |-  ( ph  ->  ( ps  <->  ch )
)
imbi12d.2  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
bibi12d  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  ta ) ) )

Proof of Theorem bibi12d
StepHypRef Expression
1 imbi12d.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21bibi1d 231 . 2  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43bibi2d 230 . 2  |-  ( ph  ->  ( ( ch  <->  th )  <->  ( ch  <->  ta ) ) )
52, 4bitrd 186 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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.32  441  bi2bian9  573  cleqh  2179  abbi  2193  cleqf  2243  vtoclb  2657  vtoclbg  2660  ceqsexg  2724  elabgf  2737  reu6  2782  ru  2815  sbcbig  2861  sbcne12g  2925  sbcnestgf  2954  preq12bg  3573  nalset  3916  opthg  4001  opelopabsb  4023  wetriext  4327  opeliunxp2  4504  resieq  4650  elimasng  4723  cbviota  4902  iota2df  4921  fnbrfvb  5246  fvelimab  5261  fmptco  5362  fsng  5368  fressnfv  5382  funfvima3  5424  isorel  5479  isocnv  5482  isocnv2  5483  isotr  5487  ovg  5670  caovcang  5693  caovordg  5699  caovord3d  5702  caovord  5703  dftpos4  5912  ecopovsym  6268  ecopovsymg  6271  xpf1o  6385  nneneq  6392  supmoti  6465  supsnti  6477  isotilem  6478  isoti  6479  ltanqg  6652  ltmnqg  6653  elinp  6726  prnmaxl  6740  prnminu  6741  ltasrg  7009  axpre-ltadd  7114  zextle  8519  zextlt  8520  rexfiuz  10013  climshft  10281  dvdsext  10400  ltoddhalfle  10437  halfleoddlt  10438  bezoutlemmo  10539  bezoutlemeu  10540  bezoutlemle  10541  bezoutlemsup  10542  dfgcd3  10543  dvdssq  10564  rpexp  10676  bj-nalset  10844  bj-d0clsepcl  10878  bj-nn0sucALT  10931
  Copyright terms: Public domain W3C validator