Theorem imbi12d 311

Description: Deduction joining two equivalences to form equivalence of implications. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbi12d.1	|- (ph -> (ps <-> ch))
imbi12d.2	|- (ph -> (th <-> ta))

Assertion

Ref	Expression
imbi12d	|- (ph -> ((ps -> th) <-> (ch -> ta)))

Proof of Theorem imbi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	imbi1d 308	. 2 |- (ph -> ((ps -> th) <-> (ch -> th)))
3		imbi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	imbi2d 307	. 2 |- (ph -> ((ch -> th) <-> (ch -> ta)))
5	2, 4	bitrd 244	1 |- (ph -> ((ps -> th) <-> (ch -> ta)))

Syntax hints:   -> wi 4   <-> wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  nfbidf  1774  drnf1  1969  drnf2  1970  equveli  1988  ax11v2  1992  ax11vALT  2097  ax10-16  2190  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  mobid  2238  2mo  2282  2eu6  2289  axext3  2336  ralcom2  2775  cbvralf  2829  cbvraldva2  2839  vtoclgaf  2919  vtocl2gaf  2921  vtocl3gaf  2923  rspct  2948  rspc  2949  ceqex  2969  ralab2  3001  mob2  3016  mob  3018  morex  3020  reu7  3031  reu8  3032  sbcimg  3087  csbhypf  3171  cbvralcsf  3198  dfss2f  3264  sbcss  3660  sneqrg  3874  elintab  3937  intss1  3941  intmin  3946  dfiin2g  4000  preqr2g  4126  ssrelk  4211  eqpw1uni  4330  iota5  4359  nnsucelr  4428  nndisjeq  4429  ltfintri  4466  lenltfin  4469  ssfin  4470  ncfinlower  4483  tfinltfinlem1  4500  evenoddnnnul  4514  evenodddisj  4516  eventfin  4517  oddtfin  4518  nnadjoin  4520  sfintfin  4532  tfinnn  4534  spfinsfincl  4539  vfinspsslem1  4550  vfinspss  4551  copsexg  4607  vtoclr  4816  ssrel  4844  ssopr  4846  tz6.12i  5348  dff13f  5472  f1fveq  5473  fununiq  5517  funsi  5520  oprabid  5550  ov3  5599  caovcan  5628  ov2gf  5711  fvmptf  5722  op1st2nd  5790  fnpprod  5843  clos1conn  5879  trd  5921  frd  5922  extd  5923  symd  5924  trrd  5925  antid  5929  iserd  5942  fundmen  6043  fundmeng  6044  enmap2  6068  enpw  6087  sbthlem2  6204  sbth  6206  taddc  6229  letc  6231  ce2le  6233  nclenn  6249  muc0or  6252  spacind  6287  nchoicelem11  6299  nchoicelem12  6300  nchoicelem17  6305  nchoicelem19  6307  frecxp  6314  fnfrec  6320