Theorem imbi2d 307

Description: Deduction adding an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
imbid.1	|- (ph -> (ps <-> ch))

Assertion

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

Proof of Theorem imbi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 |- (ph -> (ps <-> ch))
2	1	a1d 22	. 2 |- (ph -> (th -> (ps <-> ch)))
3	2	pm5.74d 238	1 |- (ph -> ((th -> ps) <-> (th -> ch)))

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

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  imbi12d  311  imbi2  314  pm5.42  531  orbi2d  682  con3th  924  19.23tOLD  1819  ax12olem6  1932  ax11v2  1992  ax15  2021  nfsb4t  2080  sbcom  2089  ax11vALT  2097  sbcom2  2114  ax11eq  2193  ax11el  2194  ax11indalem  2197  ax11inda2ALT  2198  ax11inda  2200  ax11v2-o  2201  mo  2226  2mo  2282  2eu6  2289  2gencl  2888  3gencl  2889  vtocl2gf  2916  vtocl3gf  2917  eqeu  3007  mo2icl  3015  euind  3023  reu7  3031  reuind  3039  sbctt  3108  sbcnestgf  3183  r19.36zv  3650  dedth2h  3704  dedth3h  3705  dedth4h  3706  elint  3932  elintrabg  3939  intab  3956  preq12bg  4128  nncaddccl  4419  nndisjeq  4429  ltfintri  4466  ssfin  4470  evenodddisjlem1  4515  evenodddisj  4516  nnadjoin  4520  tfinnn  4534  spfinsfincl  4539  spfininduct  4540  vtoclr  4816  raliunxp  4823  2optocl  4839  3optocl  4840  fneu  5187  fvelimab  5370  fnressn  5438  fressnfv  5439  f1fveq  5473  funsi  5520  ndmovcl  5614  caovcan  5628  caovord  5629  fvmptss  5705  trtxp  5781  oqelins4  5794  fntxp  5804  qrpprod  5836  fnpprod  5843  fnfullfunlem1  5856  frd  5922  2ecoptocl  5997  3ecoptocl  5998  sbthlem2  6204  leconnnc  6218  addcdi  6250  nchoicelem17  6305  nchoicelem19  6307