Theorem imbi1i 238

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)

Hypothesis

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

Assertion

Ref	Expression
imbi1i	|- ( ( ph -> ch ) <-> ( ps -> ch ) )

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 |- ( ph <-> ps )
2		imbi1 236	. 2 |- ( ( ph <-> ps ) -> ( ( ph -> ch ) <-> ( ps -> ch ) ) )
3	1, 2	ax-mp 5	1 |- ( ( ph -> ch ) <-> ( ps -> ch ) )

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:  imbi12i  239  ancomsimp  1451  sbrim  1972  sbal1yz  2017  sbmo  2101  mo4f  2102  moanim  2116  necon4addc  2434  necon1bddc  2441  nfraldya  2529  r3al  2538  r19.23t  2601  ceqsralt  2787  ralab  2921  ralrab  2922  euind  2948  reu2  2949  rmo4  2954  rmo3f  2958  rmo4f  2959  reuind  2966  rmo3  3078  dfdif3  3270  raldifb  3300  unss  3334  ralunb  3341  inssdif0im  3515  ssundifim  3531  raaan  3553  pwss  3618  ralsnsg  3656  ralsns  3657  disjsn  3681  snssOLD  3745  snssb  3752  unissb  3866  intun  3902  intpr  3903  dfiin2g  3946  dftr2  4130  repizf2lem  4191  axpweq  4201  zfpow  4205  axpow2  4206  zfun  4466  uniex2  4468  setindel  4571  setind  4572  elirr  4574  en2lp  4587  zfregfr  4607  tfi  4615  raliunxp  4804  dffun2  5265  dffun4  5266  dffun4f  5271  dffun7  5282  funcnveq  5318  fununi  5323  pw1dc0el  6969  fiintim  6987  addnq0mo  7509  mulnq0mo  7510  addsrmo  7805  mulsrmo  7806  prime  9419  raluz2  9647  ralrp  9744  modfsummod  11604  nnwosdc  12179  isprm4  12260  dedekindicclemicc  14811  bdcriota  15445  bj-uniex2  15478  bj-ssom  15498