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  2293  abbi  2307  cleqf  2361  cbvreuvw  2732  vtoclb  2818  vtoclbg  2822  ceqsexg  2889  elabgf  2903  reu6  2950  ru  2985  sbcbig  3033  sbcne12g  3099  sbcnestgf  3133  preq12bg  3800  nalset  4160  undifexmid  4223  exmidsssn  4232  exmidsssnc  4233  exmidundif  4236  opthg  4268  opelopabsb  4291  wetriext  4610  opeliunxp2  4803  resieq  4953  elimasng  5034  cbviota  5221  iota2df  5241  fnbrfvb  5598  fvelimab  5614  fmptco  5725  fsng  5732  fressnfv  5746  funfvima3  5793  isorel  5852  isocnv  5855  isocnv2  5856  isotr  5860  ovg  6059  caovcang  6082  caovordg  6088  caovord3d  6091  caovord  6092  uchoice  6192  opeliunxp2f  6293  dftpos4  6318  ecopovsym  6687  ecopovsymg  6690  xpf1o  6902  nneneq  6915  supmoti  7054  supsnti  7066  isotilem  7067  isoti  7068  ltanqg  7462  ltmnqg  7463  elinp  7536  prnmaxl  7550  prnminu  7551  ltasrg  7832  axpre-ltadd  7948  zextle  9411  zextlt  9412  xlesubadd  9952  rexfiuz  11136  climshft  11450  dvdsext  12000  ltoddhalfle  12037  halfleoddlt  12038  bezoutlemmo  12146  bezoutlemeu  12147  bezoutlemle  12148  bezoutlemsup  12149  dfgcd3  12150  dvdssq  12171  rpexp  12294  pcdvdsb  12461  isnsg  13275  nsgbi  13277  elnmz  13281  nmzbi  13282  nmznsg  13286  islidlm  13978  xmeteq0  14538  comet  14678  dedekindeulemuub  14796  dedekindeulemloc  14798  dedekindicclemuub  14805  dedekindicclemloc  14807  logltb  15050  bj-nalset  15457  bj-d0clsepcl  15487  bj-nn0sucALT  15540  ltlenmkv  15630