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

Assertion

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

Proof of Theorem imbi1i

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

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  1485  sbrim  2008  sbal1yz  2053  sbmo  2138  mo4f  2139  moanim  2153  necon4addc  2471  necon1bddc  2478  nfraldya  2566  r3al  2575  r19.23t  2639  ceqsralt  2829  ralab  2965  ralrab  2966  euind  2992  reu2  2993  rmo4  2998  rmo3f  3002  rmo4f  3003  reuind  3010  rmo3  3123  dfdif3  3316  raldifb  3346  unss  3380  ralunb  3387  inssdif0im  3561  ssundifim  3577  raaan  3599  pwss  3669  ralsnsg  3707  ralsns  3708  disjsn  3732  snssOLD  3800  snssb  3807  unissb  3924  intun  3960  intpr  3961  dfiin2g  4004  dftr2  4190  repizf2lem  4253  axpweq  4263  zfpow  4267  axpow2  4268  zfun  4533  uniex2  4535  setindel  4638  setind  4639  elirr  4641  en2lp  4654  zfregfr  4674  tfi  4682  raliunxp  4873  dffun2  5338  dffun4  5339  dffun4f  5344  dffun7  5355  funcnveq  5395  fununi  5400  pw1dc0el  7108  fiintim  7128  addnq0mo  7672  mulnq0mo  7673  addsrmo  7968  mulsrmo  7969  prime  9584  raluz2  9818  ralrp  9915  modfsummod  12042  nnwosdc  12633  isprm4  12714  dedekindicclemicc  15385  bdcriota  16538  bj-uniex2  16571  bj-ssom  16591  exmidpeirce  16668