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  2296  abbi  2310  cleqf  2364  cbvreuvw  2735  vtoclb  2821  vtoclbg  2825  ceqsexg  2892  elabgf  2906  reu6  2953  ru  2988  sbcbig  3036  sbcne12g  3102  sbcnestgf  3136  preq12bg  3804  nalset  4164  undifexmid  4227  exmidsssn  4236  exmidsssnc  4237  exmidundif  4240  opthg  4272  opelopabsb  4295  wetriext  4614  opeliunxp2  4807  resieq  4957  elimasng  5038  cbviota  5225  iota2df  5245  fnbrfvb  5602  fvelimab  5618  fmptco  5729  fsng  5736  fressnfv  5750  funfvima3  5797  isorel  5856  isocnv  5859  isocnv2  5860  isotr  5864  ovg  6063  caovcang  6086  caovordg  6092  caovord3d  6095  caovord  6096  uchoice  6196  opeliunxp2f  6297  dftpos4  6322  ecopovsym  6691  ecopovsymg  6694  xpf1o  6906  nneneq  6919  supmoti  7060  supsnti  7072  isotilem  7073  isoti  7074  ltanqg  7469  ltmnqg  7470  elinp  7543  prnmaxl  7557  prnminu  7558  ltasrg  7839  axpre-ltadd  7955  zextle  9419  zextlt  9420  xlesubadd  9960  rexfiuz  11156  climshft  11471  dvdsext  12022  ltoddhalfle  12060  halfleoddlt  12061  bezoutlemmo  12183  bezoutlemeu  12184  bezoutlemle  12185  bezoutlemsup  12186  dfgcd3  12187  dvdssq  12208  rpexp  12331  pcdvdsb  12499  isnsg  13342  nsgbi  13344  elnmz  13348  nmzbi  13349  nmznsg  13353  islidlm  14045  xmeteq0  14605  comet  14745  dedekindeulemuub  14863  dedekindeulemloc  14865  dedekindicclemuub  14872  dedekindicclemloc  14874  logltb  15120  bj-nalset  15551  bj-d0clsepcl  15581  bj-nn0sucALT  15634  ltlenmkv  15724