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  608  cleqh  2304  abbi  2318  cleqf  2372  cbvreuvw  2743  vtoclb  2829  vtoclbg  2833  ceqsexg  2900  elabgf  2914  reu6  2961  ru  2996  sbcbig  3044  sbcne12g  3110  sbcnestgf  3144  preq12bg  3813  nalset  4173  undifexmid  4236  exmidsssn  4245  exmidsssnc  4246  exmidundif  4249  opthg  4281  opelopabsb  4305  wetriext  4624  opeliunxp2  4817  resieq  4968  elimasng  5049  cbviota  5236  iota2df  5256  fnbrfvb  5618  fvelimab  5634  fmptco  5745  fsng  5752  fressnfv  5770  funfvima3  5817  isorel  5876  isocnv  5879  isocnv2  5880  isotr  5884  ovg  6084  caovcang  6107  caovordg  6113  caovord3d  6116  caovord  6117  uchoice  6222  opeliunxp2f  6323  dftpos4  6348  ecopovsym  6717  ecopovsymg  6720  xpf1o  6940  nneneq  6953  supmoti  7094  supsnti  7106  isotilem  7107  isoti  7108  ltanqg  7512  ltmnqg  7513  elinp  7586  prnmaxl  7600  prnminu  7601  ltasrg  7882  axpre-ltadd  7998  zextle  9463  zextlt  9464  xlesubadd  10004  rexfiuz  11271  climshft  11586  dvdsext  12137  ltoddhalfle  12175  halfleoddlt  12176  bezoutlemmo  12298  bezoutlemeu  12299  bezoutlemle  12300  bezoutlemsup  12301  dfgcd3  12302  dvdssq  12323  rpexp  12446  pcdvdsb  12614  isnsg  13509  nsgbi  13511  elnmz  13515  nmzbi  13516  nmznsg  13520  islidlm  14212  xmeteq0  14802  comet  14942  dedekindeulemuub  15060  dedekindeulemloc  15062  dedekindicclemuub  15069  dedekindicclemloc  15071  logltb  15317  bj-nalset  15793  bj-d0clsepcl  15823  bj-nn0sucALT  15876  ltlenmkv  15971