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  1486  sbrim  2010  sbal1yz  2055  sbmo  2140  mo4f  2141  moanim  2155  necon4addc  2482  necon1bddc  2489  nfraldya  2577  r3al  2586  r19.23t  2650  ceqsralt  2841  ralab  2977  ralrab  2978  euind  3004  reu2  3005  rmo4  3010  rmo3f  3014  rmo4f  3015  reuind  3022  rmo3  3135  dfdif3  3329  raldifb  3359  unss  3393  ralunb  3400  inssdif0im  3576  ssundifim  3593  raaan  3615  pwss  3688  ralsnsg  3726  ralsns  3727  disjsn  3751  snssOLD  3819  snssb  3827  unissb  3944  intun  3980  intpr  3981  dfiin2g  4024  dftr2  4210  repizf2lem  4274  axpweq  4284  zfpow  4288  axpow2  4289  zfun  4555  uniex2  4557  setindel  4660  setind  4661  elirr  4663  en2lp  4676  zfregfr  4696  tfi  4704  raliunxp  4896  dffun2  5362  dffun4  5363  dffun4f  5368  dffun7  5379  funcnveq  5419  fununi  5424  pw1dc0el  7171  fiintim  7191  addnq0mo  7762  mulnq0mo  7763  addsrmo  8058  mulsrmo  8059  prime  9677  raluz2  9911  ralrp  10008  modfsummod  12144  nnwosdc  12735  isprm4  12816  dedekindicclemicc  15497  bdcriota  16653  bj-uniex2  16686  bj-ssom  16706  exmidpeirce  16781