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  1490  sbrim  2016  sbal1yz  2061  sbmo  2146  mo4f  2147  moanim  2161  necon4addc  2490  necon1bddc  2497  nfraldya  2585  r3al  2594  r19.23t  2658  ceqsralt  2849  ralab  2986  ralrab  2987  euind  3013  reu2  3014  rmo4  3019  rmo3f  3023  rmo4f  3024  reuind  3031  rmo3  3144  dfdif3  3339  raldifb  3369  unss  3403  ralunb  3410  inssdif0im  3591  ssundifim  3608  raaan  3630  pwss  3704  ralsnsg  3742  ralsns  3743  disjsn  3767  snssOLD  3835  snssb  3843  unissb  3960  intun  3996  intpr  3997  dfiin2g  4040  dftr2  4226  repizf2lem  4293  axpweq  4303  zfpow  4307  axpow2  4308  zfun  4574  uniex2OLD  4577  setindel  4680  setind  4681  elirr  4683  en2lp  4696  zfregfr  4716  tfi  4724  raliunxp  4916  dffun2  5382  dffun4  5383  dffun4f  5388  dffun7  5399  funcnveq  5439  fununi  5444  pw1dc0el  7208  fiintim  7228  addnq0mo  7804  mulnq0mo  7805  addsrmo  8100  mulsrmo  8101  prime  9724  raluz2  9958  ralrp  10055  modfsummod  12203  nnwosdc  12794  isprm4  12875  dedekindicclemicc  15656  bdcriota  16823  bj-ssom  16876  exmidpeirce  16951