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

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	bibi1d 232	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 231	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 187	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

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  449  bi2bian9  598  cleqh  2240  abbi  2254  cleqf  2306  vtoclb  2746  vtoclbg  2750  ceqsexg  2817  elabgf  2830  reu6  2877  ru  2912  sbcbig  2959  sbcne12g  3025  sbcnestgf  3056  preq12bg  3708  nalset  4066  undifexmid  4125  exmidsssn  4133  exmidsssnc  4134  exmidundif  4137  opthg  4168  opelopabsb  4190  wetriext  4499  opeliunxp2  4687  resieq  4837  elimasng  4915  cbviota  5101  iota2df  5120  fnbrfvb  5470  fvelimab  5485  fmptco  5594  fsng  5601  fressnfv  5615  funfvima3  5659  isorel  5717  isocnv  5720  isocnv2  5721  isotr  5725  ovg  5917  caovcang  5940  caovordg  5946  caovord3d  5949  caovord  5950  opeliunxp2f  6143  dftpos4  6168  ecopovsym  6533  ecopovsymg  6536  xpf1o  6746  nneneq  6759  supmoti  6888  supsnti  6900  isotilem  6901  isoti  6902  ltanqg  7232  ltmnqg  7233  elinp  7306  prnmaxl  7320  prnminu  7321  ltasrg  7602  axpre-ltadd  7718  zextle  9166  zextlt  9167  xlesubadd  9696  rexfiuz  10793  climshft  11105  dvdsext  11589  ltoddhalfle  11626  halfleoddlt  11627  bezoutlemmo  11730  bezoutlemeu  11731  bezoutlemle  11732  bezoutlemsup  11733  dfgcd3  11734  dvdssq  11755  rpexp  11867  xmeteq0  12567  comet  12707  dedekindeulemuub  12803  dedekindeulemloc  12805  dedekindicclemuub  12812  dedekindicclemloc  12814  logltb  13003  bj-nalset  13264  bj-d0clsepcl  13294  bj-nn0sucALT  13347