Theorem imbi1i 352

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-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 350	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  ancomst  467  imor  849  ifpn  1067  eximal  1779  19.43  1879  19.37v  1994  19.37  2230  sbrim  2309  sbor  2312  dfsb3  2529  dfsb3ALT  2588  sbrimALT  2605  mo4f  2647  2mos  2730  neor  3108  r3al  3202  r19.23v  3279  r19.23t  3313  r19.43  3351  ceqsralt  3528  ralab  3683  ralrab  3684  euind  3714  reu2  3715  rmo4  3720  rmo3f  3724  rmo4f  3725  reuind  3743  2reu5lem3  3747  rmo3  3871  rmo3OLD  3872  dfdif3  4090  raldifb  4120  elunant  4153  inssdif0  4328  ssundif  4432  dfif2  4468  pwss  4558  ralsnsg  4601  disjsn  4640  snssg  4710  raldifsni  4721  raldifsnb  4722  unissb  4862  intpr  4901  dfiin2g  4949  disjor  5038  dftr2  5166  axrep1  5183  axrep6  5189  axpweq  5257  zfpow  5259  axpow2  5260  reusv2lem4  5293  reusv2  5295  raliunxp  5704  idrefALT  5967  asymref2  5971  dffun2  6359  dffun4  6361  dffun5  6362  dffun7  6376  fununi  6423  fvn0ssdmfun  6836  dff13  7007  dff14b  7023  zfun  7456  uniex2  7458  dfom2  7576  fimaxg  8759  fiint  8789  dfsup2  8902  fiming  8956  oemapso  9139  scottexs  9310  scott0s  9311  iscard2  9399  acnnum  9472  dfac9  9556  dfacacn  9561  kmlem4  9573  kmlem12  9581  axpowndlem3  10015  zfcndun  10031  zfcndpow  10032  zfcndac  10035  axgroth5  10240  axgroth6  10244  addsrmo  10489  mulsrmo  10490  infm3  11594  raluz2  12291  nnwos  12309  ralrp  12403  cotr2g  14330  lo1resb  14915  rlimresb  14916  o1resb  14917  modfsummod  15143  isprm4  16022  acsfn1  16926  acsfn2  16928  lublecllem  17592  isirred2  19445  isdomn2  20066  iunocv  20819  ist1-2  21949  isnrm2  21960  dfconn2  22021  alexsubALTlem3  22651  ismbl  24121  dyadmbllem  24194  ellimc3  24471  dchrelbas2  25807  dchrelbas3  25808  isch2  28994  choc0  29097  h1dei  29321  mdsl2i  30093  disjorf  30323  bnj1101  32051  bnj1109  32053  bnj1533  32119  bnj580  32180  bnj864  32189  bnj865  32190  bnj978  32216  bnj1049  32241  bnj1090  32246  bnj1145  32260  axextprim  32922  axunprim  32924  axpowprim  32925  untuni  32930  3orit  32940  biimpexp  32941  elintfv  33002  dfon2lem8  33030  soseq  33091  dfom5b  33368  rdgeqoa  34645  wl-equsalcom  34776  wl-dfralflem  34832  poimirlem25  34911  poimirlem30  34916  tsim1  35402  inxpss  35563  idinxpss  35564  idinxpssinxp  35568  ineleq  35602  cocossss  35675  cosscnvssid3  35710  trcoss2  35718  redundpbi1  35860  dfeldisj3  35946  cvlsupr3  36474  pmapglbx  36899  isltrn2N  37250  cdlemefrs29bpre0  37526  fphpd  39406  dford4  39619  fnwe2lem2  39644  isdomn3  39797  ifpidg  39850  ifpid1g  39853  ifpor123g  39867  dfsucon  39882  undmrnresiss  39957  elintima  39991  df3or2  40106  dfhe3  40114  dffrege76  40278  dffrege115  40317  frege131  40333  ntrneikb  40437  ismnuprim  40623  pm14.12  40746  dfvd2an  40909  dfvd3  40918  dfvd3an  40921  uun2221  41140  uun2221p1  41141  uun2221p2  41142  disjinfi  41447  supxrleubrnmptf  41720  fsummulc1f  41844  fsumiunss  41849  fnlimfvre2  41951  limsupreuz  42011  limsupvaluz2  42012  dvmptmulf  42215  dvnmul  42221  dvmptfprodlem  42222  dvnprodlem2  42225  sge0ltfirpmpt2  42702  hoidmv1le  42870  hoidmvle  42876  vonioolem2  42957  smflimlem3  43043  2reu8i  43306  ichexmpl2  43626  setrec2  44792  aacllem  44896