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  610  cleqh  2329  abbi  2343  cleqf  2397  cbvreuvw  2771  vtoclb  2859  vtoclbg  2863  ceqsexg  2932  elabgf  2946  reu6  2993  ru  3028  sbcbig  3076  sbcne12g  3143  sbcnestgf  3177  preq12bg  3854  nalset  4217  undifexmid  4281  exmidsssn  4290  exmidsssnc  4291  exmidundif  4294  opthg  4328  opelopabsb  4352  wetriext  4673  opeliunxp2  4868  resieq  5021  elimasng  5102  cbviota  5289  iota2df  5310  fnbrfvb  5680  fvelimab  5698  fmptco  5809  fsng  5816  fressnfv  5836  funfvima3  5883  isorel  5944  isocnv  5947  isocnv2  5948  isotr  5952  ovg  6156  caovcang  6179  caovordg  6185  caovord3d  6188  caovord  6189  uchoice  6295  opeliunxp2f  6399  dftpos4  6424  ecopovsym  6795  ecopovsymg  6798  xpf1o  7025  nneneq  7038  supmoti  7183  supsnti  7195  isotilem  7196  isoti  7197  ltanqg  7610  ltmnqg  7611  elinp  7684  prnmaxl  7698  prnminu  7699  ltasrg  7980  axpre-ltadd  8096  zextle  9561  zextlt  9562  xlesubadd  10108  rexfiuz  11540  climshft  11855  dvdsext  12406  ltoddhalfle  12444  halfleoddlt  12445  bezoutlemmo  12567  bezoutlemeu  12568  bezoutlemle  12569  bezoutlemsup  12570  dfgcd3  12571  dvdssq  12592  rpexp  12715  pcdvdsb  12883  isnsg  13779  nsgbi  13781  elnmz  13785  nmzbi  13786  nmznsg  13790  islidlm  14483  xmeteq0  15073  comet  15213  dedekindeulemuub  15331  dedekindeulemloc  15333  dedekindicclemuub  15340  dedekindicclemloc  15342  logltb  15588  bj-nalset  16426  bj-d0clsepcl  16456  bj-nn0sucALT  16509  ltlenmkv  16610