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  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  3893  nalset  4258  undifexmid  4325  exmidsssn  4334  exmidsssnc  4335  exmidundif  4338  opthg  4373  opelopabsb  4397  wetriext  4719  opeliunxp2  4915  resieq  5068  elimasng  5150  cbviota  5337  iota2df  5358  fnbrfvb  5735  fvelimab  5753  fmptco  5865  fsng  5872  fressnfv  5893  funfvima3  5942  isorel  6004  isocnv  6007  isocnv2  6008  isotr  6012  ovg  6218  caovcang  6241  caovordg  6247  caovord3d  6250  caovord  6251  uchoice  6361  opeliunxp2f  6499  dftpos4  6524  ecopovsym  6895  ecopovsymg  6898  xpf1o  7134  nneneq  7148  supmoti  7323  supsnti  7335  isotilem  7336  isoti  7337  ltanqg  7757  ltmnqg  7758  elinp  7831  prnmaxl  7845  prnminu  7846  ltasrg  8127  axpre-ltadd  8243  zextle  9716  zextlt  9717  xlesubadd  10264  rexfiuz  11733  climshft  12048  dvdsext  12600  ltoddhalfle  12638  halfleoddlt  12639  bezoutlemmo  12761  bezoutlemeu  12762  bezoutlemle  12763  bezoutlemsup  12764  dfgcd3  12765  dvdssq  12786  rpexp  12909  pcdvdsb  13077  isnsg  13982  nsgbi  13984  elnmz  13988  nmzbi  13989  nmznsg  13993  islidlm  14788  xmeteq0  15383  comet  15523  dedekindeulemuub  15641  dedekindeulemloc  15643  dedekindicclemuub  15650  dedekindicclemloc  15652  logltb  15898  eupth2lem3lem6fi  16626  bj-nalset  16835  bj-d0clsepcl  16865  bj-nn0sucALT  16918  ltlenmkv  17025