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  1975  sbal1yz  2020  sbmo  2104  mo4f  2105  moanim  2119  necon4addc  2437  necon1bddc  2444  nfraldya  2532  r3al  2541  r19.23t  2604  ceqsralt  2790  ralab  2924  ralrab  2925  euind  2951  reu2  2952  rmo4  2957  rmo3f  2961  rmo4f  2962  reuind  2969  rmo3  3081  dfdif3  3273  raldifb  3303  unss  3337  ralunb  3344  inssdif0im  3518  ssundifim  3534  raaan  3556  pwss  3621  ralsnsg  3659  ralsns  3660  disjsn  3684  snssOLD  3748  snssb  3755  unissb  3869  intun  3905  intpr  3906  dfiin2g  3949  dftr2  4133  repizf2lem  4194  axpweq  4204  zfpow  4208  axpow2  4209  zfun  4469  uniex2  4471  setindel  4574  setind  4575  elirr  4577  en2lp  4590  zfregfr  4610  tfi  4618  raliunxp  4807  dffun2  5268  dffun4  5269  dffun4f  5274  dffun7  5285  funcnveq  5321  fununi  5326  pw1dc0el  6972  fiintim  6992  addnq0mo  7514  mulnq0mo  7515  addsrmo  7810  mulsrmo  7811  prime  9425  raluz2  9653  ralrp  9750  modfsummod  11623  nnwosdc  12206  isprm4  12287  dedekindicclemicc  14868  bdcriota  15529  bj-uniex2  15562  bj-ssom  15582