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  4263  undifexmid  4330  exmidsssn  4339  exmidsssnc  4340  exmidundif  4343  opthg  4378  opelopabsb  4402  wetriext  4724  opeliunxp2  4920  resieq  5073  elimasng  5155  cbviota  5342  iota2df  5363  fnbrfvb  5741  fvelimab  5759  fmptco  5874  fsng  5881  fressnfv  5902  funfvima3  5952  isorel  6014  isocnv  6017  isocnv2  6018  isotr  6022  ovg  6228  caovcang  6251  caovordg  6257  caovord3d  6260  caovord  6261  uchoice  6371  opeliunxp2f  6509  dftpos4  6534  ecopovsym  6905  ecopovsymg  6908  xpf1o  7144  nneneq  7158  supmoti  7333  supsnti  7345  isotilem  7346  isoti  7347  ltanqg  7767  ltmnqg  7768  elinp  7841  prnmaxl  7855  prnminu  7856  ltasrg  8137  axpre-ltadd  8253  zextle  9741  zextlt  9742  xlesubadd  10295  rexfiuz  11769  climshft  12086  dvdsext  12638  ltoddhalfle  12676  halfleoddlt  12677  bezoutlemmo  12799  bezoutlemeu  12800  bezoutlemle  12801  bezoutlemsup  12802  dfgcd3  12803  dvdssq  12824  rpexp  12948  pcdvdsb  13119  isnsg  14054  nsgbi  14056  elnmz  14060  nmzbi  14061  nmznsg  14065  islidlm  14865  xmeteq0  15509  comet  15649  dedekindeulemuub  15767  dedekindeulemloc  15769  dedekindicclemuub  15776  dedekindicclemloc  15778  logltb  16026  eupth2lem3lem6fi  16810  bj-nalset  17019  bj-d0clsepcl  17049  bj-nn0sucALT  17102  ltlenmkv  17218