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  2289  abbi  2303  cleqf  2357  cbvreuvw  2724  vtoclb  2809  vtoclbg  2813  ceqsexg  2880  elabgf  2894  reu6  2941  ru  2976  sbcbig  3024  sbcne12g  3090  sbcnestgf  3123  preq12bg  3788  nalset  4148  undifexmid  4208  exmidsssn  4217  exmidsssnc  4218  exmidundif  4221  opthg  4253  opelopabsb  4275  wetriext  4591  opeliunxp2  4782  resieq  4932  elimasng  5011  cbviota  5198  iota2df  5217  fnbrfvb  5572  fvelimab  5588  fmptco  5698  fsng  5705  fressnfv  5719  funfvima3  5766  isorel  5825  isocnv  5828  isocnv2  5829  isotr  5833  ovg  6030  caovcang  6053  caovordg  6059  caovord3d  6062  caovord  6063  opeliunxp2f  6257  dftpos4  6282  ecopovsym  6649  ecopovsymg  6652  xpf1o  6862  nneneq  6875  supmoti  7010  supsnti  7022  isotilem  7023  isoti  7024  ltanqg  7417  ltmnqg  7418  elinp  7491  prnmaxl  7505  prnminu  7506  ltasrg  7787  axpre-ltadd  7903  zextle  9362  zextlt  9363  xlesubadd  9901  rexfiuz  11016  climshft  11330  dvdsext  11879  ltoddhalfle  11916  halfleoddlt  11917  bezoutlemmo  12025  bezoutlemeu  12026  bezoutlemle  12027  bezoutlemsup  12028  dfgcd3  12029  dvdssq  12050  rpexp  12171  pcdvdsb  12337  isnsg  13107  nsgbi  13109  elnmz  13113  nmzbi  13114  nmznsg  13118  islidlm  13756  xmeteq0  14256  comet  14396  dedekindeulemuub  14492  dedekindeulemloc  14494  dedekindicclemuub  14501  dedekindicclemloc  14503  logltb  14692  bj-nalset  15044  bj-d0clsepcl  15074  bj-nn0sucALT  15127  ltlenmkv  15216