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-mp 5  ax-1 6  ax-2 7  ax-3 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  2889  3gencl  2890  vtocl2gf  2917  vtocl3gf  2918  eqeu  3008  mo2icl  3016  euind  3024  reu7  3032  reuind  3040  sbctt  3109  sbcnestgf  3184  r19.36zv  3651  dedth2h  3705  dedth3h  3706  dedth4h  3707  elint  3933  elintrabg  3940  intab  3957  preq12bg  4129  nncaddccl  4420  nndisjeq  4430  ltfintri  4467  ssfin  4471  evenodddisjlem1  4516  evenodddisj  4517  nnadjoin  4521  tfinnn  4535  spfinsfincl  4540  spfininduct  4541  vtoclr  4817  raliunxp  4824  2optocl  4840  3optocl  4841  fneu  5188  fvelimab  5371  fnressn  5439  fressnfv  5440  f1fveq  5474  funsi  5521  ndmovcl  5615  caovcan  5629  caovord  5630  fvmptss  5706  trtxp  5782  oqelins4  5795  fntxp  5805  qrpprod  5837  fnpprod  5844  fnfullfunlem1  5857  frd  5923  2ecoptocl  5998  3ecoptocl  5999  sbthlem2  6205  leconnnc  6219  addcdi  6251  nchoicelem17  6306  nchoicelem19  6308