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 ) ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.32  457  bi2bian9  616  cleqh  2338  abbibcom  2352  abbib  2356  cleqf  2417  cbvreuvw  2792  vtoclb  2880  vtoclbg  2884  ceqsexg  2954  elabgf  2968  reu6  3015  ru  3050  sbcbig  3098  sbcne12g  3165  sbcnestgf  3199  preq12bg  3898  nalset  4265  undifexmid  4332  exmidsssn  4341  exmidsssnc  4342  exmidundif  4345  opthg  4380  opelopabsb  4404  wetriext  4726  opeliunxp2  4922  resieq  5075  elimasng  5158  cbviota  5345  iota2df  5366  fnbrfvb  5744  fvelimab  5762  fmptco  5877  fsng  5884  fressnfv  5905  funfvima3  5955  isorel  6017  isocnv  6020  isocnv2  6021  isotr  6025  ovg  6231  caovcang  6254  caovordg  6260  caovord3d  6263  caovord  6264  uchoice  6375  opeliunxp2f  6514  dftpos4  6539  ecopovsym  6910  ecopovsymg  6913  xpf1o  7150  nneneq  7164  supmoti  7339  supsnti  7351  isotilem  7352  isoti  7353  ltanqg  7773  ltmnqg  7774  elinp  7847  prnmaxl  7861  prnminu  7862  ltasrg  8143  axpre-ltadd  8259  zextle  9747  zextlt  9748  xlesubadd  10301  rexfiuz  11776  climshft  12094  dvdsext  12646  ltoddhalfle  12684  halfleoddlt  12685  bezoutlemmo  12807  bezoutlemeu  12808  bezoutlemle  12809  bezoutlemsup  12810  dfgcd3  12811  dvdssq  12832  rpexp  12956  pcdvdsb  13127  isnsg  14063  nsgbi  14065  elnmz  14069  nmzbi  14070  nmznsg  14074  gsumcom2fi  14274  islidlm  14924  xmeteq0  15602  comet  15742  dedekindeulemuub  15860  dedekindeulemloc  15862  dedekindicclemuub  15869  dedekindicclemloc  15871  logltb  16121  eupth2lem3lem6fi  16934  bj-nalset  17143  bj-d0clsepcl  17173  bj-nn0sucALT  17226  ltlenmkv  17344