Theorem imbi1i 237

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 235	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12i  238  ancomsimp  1433  sbrim  1949  sbal1yz  1994  sbmo  2078  mo4f  2079  moanim  2093  necon4addc  2410  necon1bddc  2417  nfraldya  2505  r3al  2514  r19.23t  2577  ceqsralt  2757  ralab  2890  ralrab  2891  euind  2917  reu2  2918  rmo4  2923  rmo3f  2927  rmo4f  2928  reuind  2935  rmo3  3046  dfdif3  3237  raldifb  3267  unss  3301  ralunb  3308  inssdif0im  3482  ssundifim  3498  raaan  3521  pwss  3582  ralsnsg  3620  ralsns  3621  disjsn  3645  snss  3709  unissb  3826  intun  3862  intpr  3863  dfiin2g  3906  dftr2  4089  repizf2lem  4147  axpweq  4157  zfpow  4161  axpow2  4162  zfun  4419  uniex2  4421  setindel  4522  setind  4523  elirr  4525  en2lp  4538  zfregfr  4558  tfi  4566  raliunxp  4752  dffun2  5208  dffun4  5209  dffun4f  5214  dffun7  5225  funcnveq  5261  fununi  5266  pw1dc0el  6889  fiintim  6906  addnq0mo  7409  mulnq0mo  7410  addsrmo  7705  mulsrmo  7706  prime  9311  raluz2  9538  ralrp  9632  modfsummod  11421  nnwosdc  11994  isprm4  12073  dedekindicclemicc  13404  bdcriota  13918  bj-uniex2  13951  bj-ssom  13971