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  7334  supsnti  7346  isotilem  7347  isoti  7348  ltanqg  7768  ltmnqg  7769  elinp  7842  prnmaxl  7856  prnminu  7857  ltasrg  8138  axpre-ltadd  8254  zextle  9742  zextlt  9743  xlesubadd  10296  rexfiuz  11771  climshft  12089  dvdsext  12641  ltoddhalfle  12679  halfleoddlt  12680  bezoutlemmo  12802  bezoutlemeu  12803  bezoutlemle  12804  bezoutlemsup  12805  dfgcd3  12806  dvdssq  12827  rpexp  12951  pcdvdsb  13122  isnsg  14058  nsgbi  14060  elnmz  14064  nmzbi  14065  nmznsg  14069  islidlm  14900  xmeteq0  15551  comet  15691  dedekindeulemuub  15809  dedekindeulemloc  15811  dedekindicclemuub  15818  dedekindicclemloc  15820  logltb  16068  eupth2lem3lem6fi  16878  bj-nalset  17087  bj-d0clsepcl  17117  bj-nn0sucALT  17170  ltlenmkv  17287