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  9737  zextlt  9738  xlesubadd  10285  rexfiuz  11755  climshft  12070  dvdsext  12622  ltoddhalfle  12660  halfleoddlt  12661  bezoutlemmo  12783  bezoutlemeu  12784  bezoutlemle  12785  bezoutlemsup  12786  dfgcd3  12787  dvdssq  12808  rpexp  12931  pcdvdsb  13099  isnsg  14005  nsgbi  14007  elnmz  14011  nmzbi  14012  nmznsg  14016  islidlm  14816  xmeteq0  15460  comet  15600  dedekindeulemuub  15718  dedekindeulemloc  15720  dedekindicclemuub  15727  dedekindicclemloc  15729  logltb  15975  eupth2lem3lem6fi  16712  bj-nalset  16921  bj-d0clsepcl  16951  bj-nn0sucALT  17004  ltlenmkv  17120