Theorem imbi1i 227

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	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
imbi1i	⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Proof of Theorem imbi1i

Step	Hyp	Ref	Expression
1		imbi1i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		imbi1 225	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 7	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  imbi12i  228  ancomsimp  1329  sbrim  1830  sbal1yz  1877  sbmo  1959  mo4f  1960  moanim  1974  necon4addc  2275  necon1bddc  2282  nfraldya  2358  r3al  2366  r19.23t  2423  ceqsralt  2581  ralab  2701  ralrab  2702  euind  2728  reu2  2729  rmo4  2734  reuind  2744  rmo3  2849  raldifb  3083  unss  3117  ralunb  3124  inssdif0im  3291  ssundifim  3306  raaan  3327  pwss  3374  ralsnsg  3407  ralsns  3408  disjsn  3432  snss  3494  unissb  3610  intun  3646  intpr  3647  dfiin2g  3690  dftr2  3856  repizf2lem  3914  axpweq  3924  zfpow  3928  axpow2  3929  zfun  4171  uniex2  4173  setindel  4263  setind  4264  elirr  4266  en2lp  4278  zfregfr  4298  tfi  4305  raliunxp  4477  dffun2  4912  dffun4  4913  dffun4f  4918  dffun7  4928  funcnveq  4962  fununi  4967  addnq0mo  6545  mulnq0mo  6546  addsrmo  6828  mulsrmo  6829  prime  8337  raluz2  8522  ralrp  8604  bdcriota  10003  bj-uniex2  10036  bj-ssom  10060