Theorem bibi12d 235

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 233	. 2 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )
3		imbi12d.2	. . 3 |- ( ph -> ( th <-> ta ) )
4	3	bibi2d 232	. 2 |- ( ph -> ( ( ch <-> th ) <-> ( ch <-> ta ) ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( ( ps <-> th ) <-> ( ch <-> ta ) ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32  453  bi2bian9  610  cleqh  2329  abbi  2343  cleqf  2397  cbvreuvw  2771  vtoclb  2858  vtoclbg  2862  ceqsexg  2931  elabgf  2945  reu6  2992  ru  3027  sbcbig  3075  sbcne12g  3142  sbcnestgf  3176  preq12bg  3850  nalset  4213  undifexmid  4276  exmidsssn  4285  exmidsssnc  4286  exmidundif  4289  opthg  4323  opelopabsb  4347  wetriext  4668  opeliunxp2  4861  resieq  5014  elimasng  5095  cbviota  5282  iota2df  5303  fnbrfvb  5671  fvelimab  5689  fmptco  5800  fsng  5807  fressnfv  5825  funfvima3  5872  isorel  5931  isocnv  5934  isocnv2  5935  isotr  5939  ovg  6143  caovcang  6166  caovordg  6172  caovord3d  6175  caovord  6176  uchoice  6281  opeliunxp2f  6382  dftpos4  6407  ecopovsym  6776  ecopovsymg  6779  xpf1o  7001  nneneq  7014  supmoti  7156  supsnti  7168  isotilem  7169  isoti  7170  ltanqg  7583  ltmnqg  7584  elinp  7657  prnmaxl  7671  prnminu  7672  ltasrg  7953  axpre-ltadd  8069  zextle  9534  zextlt  9535  xlesubadd  10075  rexfiuz  11495  climshft  11810  dvdsext  12361  ltoddhalfle  12399  halfleoddlt  12400  bezoutlemmo  12522  bezoutlemeu  12523  bezoutlemle  12524  bezoutlemsup  12525  dfgcd3  12526  dvdssq  12547  rpexp  12670  pcdvdsb  12838  isnsg  13734  nsgbi  13736  elnmz  13740  nmzbi  13741  nmznsg  13745  islidlm  14437  xmeteq0  15027  comet  15167  dedekindeulemuub  15285  dedekindeulemloc  15287  dedekindicclemuub  15294  dedekindicclemloc  15296  logltb  15542  bj-nalset  16216  bj-d0clsepcl  16246  bj-nn0sucALT  16299  ltlenmkv  16397