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  2304  abbi  2318  cleqf  2372  cbvreuvw  2743  vtoclb  2829  vtoclbg  2833  ceqsexg  2900  elabgf  2914  reu6  2961  ru  2996  sbcbig  3044  sbcne12g  3110  sbcnestgf  3144  preq12bg  3813  nalset  4173  undifexmid  4236  exmidsssn  4245  exmidsssnc  4246  exmidundif  4249  opthg  4281  opelopabsb  4305  wetriext  4624  opeliunxp2  4817  resieq  4968  elimasng  5049  cbviota  5236  iota2df  5256  fnbrfvb  5618  fvelimab  5634  fmptco  5745  fsng  5752  fressnfv  5770  funfvima3  5817  isorel  5876  isocnv  5879  isocnv2  5880  isotr  5884  ovg  6084  caovcang  6107  caovordg  6113  caovord3d  6116  caovord  6117  uchoice  6222  opeliunxp2f  6323  dftpos4  6348  ecopovsym  6717  ecopovsymg  6720  xpf1o  6940  nneneq  6953  supmoti  7094  supsnti  7106  isotilem  7107  isoti  7108  ltanqg  7512  ltmnqg  7513  elinp  7586  prnmaxl  7600  prnminu  7601  ltasrg  7882  axpre-ltadd  7998  zextle  9463  zextlt  9464  xlesubadd  10004  rexfiuz  11242  climshft  11557  dvdsext  12108  ltoddhalfle  12146  halfleoddlt  12147  bezoutlemmo  12269  bezoutlemeu  12270  bezoutlemle  12271  bezoutlemsup  12272  dfgcd3  12273  dvdssq  12294  rpexp  12417  pcdvdsb  12585  isnsg  13480  nsgbi  13482  elnmz  13486  nmzbi  13487  nmznsg  13491  islidlm  14183  xmeteq0  14773  comet  14913  dedekindeulemuub  15031  dedekindeulemloc  15033  dedekindicclemuub  15040  dedekindicclemloc  15042  logltb  15288  bj-nalset  15764  bj-d0clsepcl  15794  bj-nn0sucALT  15847  ltlenmkv  15942