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  2009  sbal1yz  2054  sbmo  2139  mo4f  2140  moanim  2154  necon4addc  2473  necon1bddc  2480  nfraldya  2568  r3al  2577  r19.23t  2641  ceqsralt  2831  ralab  2967  ralrab  2968  euind  2994  reu2  2995  rmo4  3000  rmo3f  3004  rmo4f  3005  reuind  3012  rmo3  3125  dfdif3  3319  raldifb  3349  unss  3383  ralunb  3390  inssdif0im  3564  ssundifim  3580  raaan  3602  pwss  3672  ralsnsg  3710  ralsns  3711  disjsn  3735  snssOLD  3803  snssb  3811  unissb  3928  intun  3964  intpr  3965  dfiin2g  4008  dftr2  4194  repizf2lem  4257  axpweq  4267  zfpow  4271  axpow2  4272  zfun  4537  uniex2  4539  setindel  4642  setind  4643  elirr  4645  en2lp  4658  zfregfr  4678  tfi  4686  raliunxp  4877  dffun2  5343  dffun4  5344  dffun4f  5349  dffun7  5360  funcnveq  5400  fununi  5405  pw1dc0el  7146  fiintim  7166  addnq0mo  7727  mulnq0mo  7728  addsrmo  8023  mulsrmo  8024  prime  9640  raluz2  9874  ralrp  9971  modfsummod  12099  nnwosdc  12690  isprm4  12771  dedekindicclemicc  15443  bdcriota  16599  bj-uniex2  16632  bj-ssom  16652  exmidpeirce  16729