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

Theorem bibi12d 234
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 232 . 2  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  th ) ) )
3 imbi12d.2 . . 3  |-  ( ph  ->  ( th  <->  ta )
)
43bibi2d 231 . 2  |-  ( ph  ->  ( ( ch  <->  th )  <->  ( ch  <->  ta ) ) )
52, 4bitrd 187 1  |-  ( ph  ->  ( ( ps  <->  th )  <->  ( ch  <->  ta ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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:  pm5.32  448  bi2bian9  597  cleqh  2239  abbi  2253  cleqf  2305  vtoclb  2743  vtoclbg  2747  ceqsexg  2813  elabgf  2826  reu6  2873  ru  2908  sbcbig  2955  sbcne12g  3020  sbcnestgf  3051  preq12bg  3700  nalset  4058  undifexmid  4117  exmidsssn  4125  exmidsssnc  4126  exmidundif  4129  opthg  4160  opelopabsb  4182  wetriext  4491  opeliunxp2  4679  resieq  4829  elimasng  4907  cbviota  5093  iota2df  5112  fnbrfvb  5462  fvelimab  5477  fmptco  5586  fsng  5593  fressnfv  5607  funfvima3  5651  isorel  5709  isocnv  5712  isocnv2  5713  isotr  5717  ovg  5909  caovcang  5932  caovordg  5938  caovord3d  5941  caovord  5942  opeliunxp2f  6135  dftpos4  6160  ecopovsym  6525  ecopovsymg  6528  xpf1o  6738  nneneq  6751  supmoti  6880  supsnti  6892  isotilem  6893  isoti  6894  ltanqg  7222  ltmnqg  7223  elinp  7296  prnmaxl  7310  prnminu  7311  ltasrg  7592  axpre-ltadd  7708  zextle  9156  zextlt  9157  xlesubadd  9680  rexfiuz  10775  climshft  11087  dvdsext  11566  ltoddhalfle  11603  halfleoddlt  11604  bezoutlemmo  11707  bezoutlemeu  11708  bezoutlemle  11709  bezoutlemsup  11710  dfgcd3  11711  dvdssq  11732  rpexp  11844  xmeteq0  12544  comet  12684  dedekindeulemuub  12780  dedekindeulemloc  12782  dedekindicclemuub  12789  dedekindicclemloc  12791  logltb  12979  bj-nalset  13200  bj-d0clsepcl  13230  bj-nn0sucALT  13283
  Copyright terms: Public domain W3C validator