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  1483  sbrim  2007  sbal1yz  2052  sbmo  2137  mo4f  2138  moanim  2152  necon4addc  2470  necon1bddc  2477  nfraldya  2565  r3al  2574  r19.23t  2638  ceqsralt  2827  ralab  2963  ralrab  2964  euind  2990  reu2  2991  rmo4  2996  rmo3f  3000  rmo4f  3001  reuind  3008  rmo3  3121  dfdif3  3314  raldifb  3344  unss  3378  ralunb  3385  inssdif0im  3559  ssundifim  3575  raaan  3597  pwss  3665  ralsnsg  3703  ralsns  3704  disjsn  3728  snssOLD  3794  snssb  3801  unissb  3918  intun  3954  intpr  3955  dfiin2g  3998  dftr2  4184  repizf2lem  4245  axpweq  4255  zfpow  4259  axpow2  4260  zfun  4525  uniex2  4527  setindel  4630  setind  4631  elirr  4633  en2lp  4646  zfregfr  4666  tfi  4674  raliunxp  4863  dffun2  5328  dffun4  5329  dffun4f  5334  dffun7  5345  funcnveq  5384  fununi  5389  pw1dc0el  7073  fiintim  7093  addnq0mo  7634  mulnq0mo  7635  addsrmo  7930  mulsrmo  7931  prime  9546  raluz2  9774  ralrp  9871  modfsummod  11969  nnwosdc  12560  isprm4  12641  dedekindicclemicc  15306  bdcriota  16246  bj-uniex2  16279  bj-ssom  16299