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  2776  cbvralf  2830  cbvraldva2  2840  vtoclgaf  2920  vtocl2gaf  2922  vtocl3gaf  2924  rspct  2949  rspc  2950  ceqex  2970  ralab2  3002  mob2  3017  mob  3019  morex  3021  reu7  3032  reu8  3033  sbcimg  3088  csbhypf  3172  cbvralcsf  3199  dfss2f  3265  sbcss  3661  sneqrg  3875  elintab  3938  intss1  3942  intmin  3947  dfiin2g  4001  preqr2g  4127  ssrelk  4212  eqpw1uni  4331  iota5  4360  nnsucelr  4429  nndisjeq  4430  ltfintri  4467  lenltfin  4470  ssfin  4471  ncfinlower  4484  tfinltfinlem1  4501  evenoddnnnul  4515  evenodddisj  4517  eventfin  4518  oddtfin  4519  nnadjoin  4521  sfintfin  4533  tfinnn  4535  spfinsfincl  4540  vfinspsslem1  4551  vfinspss  4552  copsexg  4608  vtoclr  4817  ssrel  4845  ssopr  4847  tz6.12i  5349  dff13f  5473  f1fveq  5474  fununiq  5518  funsi  5521  oprabid  5551  ov3  5600  caovcan  5629  ov2gf  5712  fvmptf  5723  op1st2nd  5791  fnpprod  5844  clos1conn  5880  trd  5922  frd  5923  extd  5924  symd  5925  trrd  5926  antid  5930  iserd  5943  fundmen  6044  fundmeng  6045  enmap2  6069  enpw  6088  sbthlem2  6205  sbth  6207  taddc  6230  letc  6232  ce2le  6234  nclenn  6250  muc0or  6253  spacind  6288  nchoicelem11  6300  nchoicelem12  6301  nchoicelem17  6306  nchoicelem19  6308  frecxp  6315  fnfrec  6321