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  1440  sbrim  1956  sbal1yz  2001  sbmo  2085  mo4f  2086  moanim  2100  necon4addc  2417  necon1bddc  2424  nfraldya  2512  r3al  2521  r19.23t  2584  ceqsralt  2766  ralab  2899  ralrab  2900  euind  2926  reu2  2927  rmo4  2932  rmo3f  2936  rmo4f  2937  reuind  2944  rmo3  3056  dfdif3  3247  raldifb  3277  unss  3311  ralunb  3318  inssdif0im  3492  ssundifim  3508  raaan  3531  pwss  3593  ralsnsg  3631  ralsns  3632  disjsn  3656  snssOLD  3720  snssb  3727  unissb  3841  intun  3877  intpr  3878  dfiin2g  3921  dftr2  4105  repizf2lem  4163  axpweq  4173  zfpow  4177  axpow2  4178  zfun  4436  uniex2  4438  setindel  4539  setind  4540  elirr  4542  en2lp  4555  zfregfr  4575  tfi  4583  raliunxp  4770  dffun2  5228  dffun4  5229  dffun4f  5234  dffun7  5245  funcnveq  5281  fununi  5286  pw1dc0el  6913  fiintim  6930  addnq0mo  7448  mulnq0mo  7449  addsrmo  7744  mulsrmo  7745  prime  9354  raluz2  9581  ralrp  9677  modfsummod  11468  nnwosdc  12042  isprm4  12121  dedekindicclemicc  14149  bdcriota  14674  bj-uniex2  14707  bj-ssom  14727