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  3851  nalset  4214  undifexmid  4277  exmidsssn  4286  exmidsssnc  4287  exmidundif  4290  opthg  4324  opelopabsb  4348  wetriext  4669  opeliunxp2  4862  resieq  5015  elimasng  5096  cbviota  5283  iota2df  5304  fnbrfvb  5674  fvelimab  5692  fmptco  5803  fsng  5810  fressnfv  5830  funfvima3  5877  isorel  5938  isocnv  5941  isocnv2  5942  isotr  5946  ovg  6150  caovcang  6173  caovordg  6179  caovord3d  6182  caovord  6183  uchoice  6289  opeliunxp2f  6390  dftpos4  6415  ecopovsym  6786  ecopovsymg  6789  xpf1o  7013  nneneq  7026  supmoti  7171  supsnti  7183  isotilem  7184  isoti  7185  ltanqg  7598  ltmnqg  7599  elinp  7672  prnmaxl  7686  prnminu  7687  ltasrg  7968  axpre-ltadd  8084  zextle  9549  zextlt  9550  xlesubadd  10091  rexfiuz  11515  climshft  11830  dvdsext  12381  ltoddhalfle  12419  halfleoddlt  12420  bezoutlemmo  12542  bezoutlemeu  12543  bezoutlemle  12544  bezoutlemsup  12545  dfgcd3  12546  dvdssq  12567  rpexp  12690  pcdvdsb  12858  isnsg  13754  nsgbi  13756  elnmz  13760  nmzbi  13761  nmznsg  13765  islidlm  14458  xmeteq0  15048  comet  15188  dedekindeulemuub  15306  dedekindeulemloc  15308  dedekindicclemuub  15315  dedekindicclemloc  15317  logltb  15563  bj-nalset  16313  bj-d0clsepcl  16343  bj-nn0sucALT  16396  ltlenmkv  16498