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  1783  19.43  1883  19.37v  1998  19.37  2234  sbrim  2313  sbor  2316  dfsb3  2533  dfsb3ALT  2592  sbrimALT  2609  mo4f  2651  2mos  2734  neor  3108  r3al  3202  r19.23v  3279  r19.23t  3313  r19.43  3351  ceqsralt  3528  ralab  3684  ralrab  3685  euind  3715  reu2  3716  rmo4  3721  rmo3f  3725  rmo4f  3726  reuind  3744  2reu5lem3  3748  rmo3  3872  rmo3OLD  3873  dfdif3  4091  raldifb  4121  elunant  4154  inssdif0  4329  ssundif  4433  dfif2  4469  pwss  4564  ralsnsg  4608  disjsn  4647  snssg  4717  raldifsni  4728  raldifsnb  4729  unissb  4870  intpr  4909  dfiin2g  4957  disjor  5046  dftr2  5174  axrep1  5191  axrep6  5197  axpweq  5265  zfpow  5267  axpow2  5268  reusv2lem4  5302  reusv2  5304  raliunxp  5710  idrefALT  5973  asymref2  5977  dffun2  6365  dffun4  6367  dffun5  6368  dffun7  6382  fununi  6429  fvn0ssdmfun  6842  dff13  7013  dff14b  7029  zfun  7462  uniex2  7464  dfom2  7582  fimaxg  8765  fiint  8795  dfsup2  8908  fiming  8962  oemapso  9145  scottexs  9316  scott0s  9317  iscard2  9405  acnnum  9478  dfac9  9562  dfacacn  9567  kmlem4  9579  kmlem12  9587  axpowndlem3  10021  zfcndun  10037  zfcndpow  10038  zfcndac  10041  axgroth5  10246  axgroth6  10250  addsrmo  10495  mulsrmo  10496  infm3  11600  raluz2  12298  nnwos  12316  ralrp  12410  cotr2g  14336  lo1resb  14921  rlimresb  14922  o1resb  14923  modfsummod  15149  isprm4  16028  acsfn1  16932  acsfn2  16934  lublecllem  17598  isirred2  19451  isdomn2  20072  iunocv  20825  ist1-2  21955  isnrm2  21966  dfconn2  22027  alexsubALTlem3  22657  ismbl  24127  dyadmbllem  24200  ellimc3  24477  dchrelbas2  25813  dchrelbas3  25814  isch2  29000  choc0  29103  h1dei  29327  mdsl2i  30099  disjorf  30329  bnj1101  32056  bnj1109  32058  bnj1533  32124  bnj580  32185  bnj864  32194  bnj865  32195  bnj978  32221  bnj1049  32246  bnj1090  32251  bnj1145  32265  axextprim  32927  axunprim  32929  axpowprim  32930  untuni  32935  3orit  32945  biimpexp  32946  elintfv  33007  dfon2lem8  33035  soseq  33096  dfom5b  33373  rdgeqoa  34654  wl-equsalcom  34797  wl-dfralflem  34853  poimirlem25  34932  poimirlem30  34937  tsim1  35423  inxpss  35584  idinxpss  35585  idinxpssinxp  35589  ineleq  35623  cocossss  35696  cosscnvssid3  35731  trcoss2  35739  redundpbi1  35881  dfeldisj3  35967  cvlsupr3  36495  pmapglbx  36920  isltrn2N  37271  cdlemefrs29bpre0  37547  fphpd  39462  dford4  39675  fnwe2lem2  39700  isdomn3  39853  ifpidg  39906  ifpid1g  39909  ifpor123g  39923  dfsucon  39938  undmrnresiss  40013  elintima  40047  df3or2  40162  dfhe3  40170  dffrege76  40334  dffrege115  40373  frege131  40389  ntrneikb  40493  ismnuprim  40679  pm14.12  40802  dfvd2an  40965  dfvd3  40974  dfvd3an  40977  uun2221  41196  uun2221p1  41197  uun2221p2  41198  disjinfi  41503  supxrleubrnmptf  41776  fsummulc1f  41900  fsumiunss  41905  fnlimfvre2  42007  limsupreuz  42067  limsupvaluz2  42068  dvmptmulf  42271  dvnmul  42277  dvmptfprodlem  42278  dvnprodlem2  42281  sge0ltfirpmpt2  42757  hoidmv1le  42925  hoidmvle  42931  vonioolem2  43012  smflimlem3  43098  2reu8i  43361  ichexmpl2  43681  setrec2  44847  aacllem  44951