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  612  cleqh  2334  abbibcom  2348  abbib  2352  cleqf  2411  cbvreuvw  2786  vtoclb  2874  vtoclbg  2878  ceqsexg  2948  elabgf  2962  reu6  3009  ru  3044  sbcbig  3092  sbcne12g  3159  sbcnestgf  3193  preq12bg  3882  nalset  4245  undifexmid  4311  exmidsssn  4320  exmidsssnc  4321  exmidundif  4324  opthg  4359  opelopabsb  4383  wetriext  4704  opeliunxp2  4900  resieq  5053  elimasng  5135  cbviota  5322  iota2df  5343  fnbrfvb  5720  fvelimab  5738  fmptco  5848  fsng  5855  fressnfv  5876  funfvima3  5925  isorel  5987  isocnv  5990  isocnv2  5991  isotr  5995  ovg  6201  caovcang  6224  caovordg  6230  caovord3d  6233  caovord  6234  uchoice  6344  opeliunxp2f  6482  dftpos4  6507  ecopovsym  6878  ecopovsymg  6881  xpf1o  7110  nneneq  7124  supmoti  7297  supsnti  7309  isotilem  7310  isoti  7311  ltanqg  7731  ltmnqg  7732  elinp  7805  prnmaxl  7819  prnminu  7820  ltasrg  8101  axpre-ltadd  8217  zextle  9687  zextlt  9688  xlesubadd  10235  rexfiuz  11699  climshft  12014  dvdsext  12566  ltoddhalfle  12604  halfleoddlt  12605  bezoutlemmo  12727  bezoutlemeu  12728  bezoutlemle  12729  bezoutlemsup  12730  dfgcd3  12731  dvdssq  12752  rpexp  12875  pcdvdsb  13043  isnsg  13955  nsgbi  13957  elnmz  13961  nmzbi  13962  nmznsg  13966  islidlm  14753  xmeteq0  15350  comet  15490  dedekindeulemuub  15608  dedekindeulemloc  15610  dedekindicclemuub  15617  dedekindicclemloc  15619  logltb  15865  eupth2lem3lem6fi  16592  bj-nalset  16791  bj-d0clsepcl  16821  bj-nn0sucALT  16874  ltlenmkv  16982