Theorem imbi1i 349

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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  ancomst  464  imor  854  3jaob  1428  eximal  1782  nfnbi  1855  19.43  1882  19.37v  1991  19.37  2232  sbrimOLD  2305  sbor  2307  sb8v  2355  sb8f  2356  dfsb3  2499  mo4f  2567  2mos  2649  2mosOLD  2650  neor  3034  r19.43  3122  r19.23v  3183  r3al  3197  r19.23t  3255  sbralie  3358  ceqsralt  3516  ralab  3697  ralabOLD  3698  ralrab  3699  euind  3730  reu2  3731  rmo4  3736  rmo3f  3740  rmo4f  3741  reuind  3759  2reu5lem3  3763  rmo3  3889  dfdif3OLD  4118  raldifb  4149  elunant  4184  ralin  4249  inssdif0  4374  ssundif  4488  dfif2  4527  pwss  4623  ralsnsg  4670  ralsng  4675  disjsn  4711  snssb  4782  snssgOLD  4784  raldifsni  4795  raldifsnb  4796  unissb  4939  unissbOLD  4940  intprg  4981  dfiin2g  5032  disjor  5125  dftr2  5261  axrep1  5280  axrep4v  5284  axrep4  5285  axrep6OLD  5289  axpweq  5351  zfpow  5366  axpow2  5367  reusv2lem4  5401  reusv2  5403  el  5442  dffr6  5640  raliunxp  5850  cotrg  6127  cotrgOLD  6128  idrefALT  6131  cnvsym  6132  cnvsymOLD  6133  asymref2  6137  dffun2OLDOLD  6573  dffun4  6577  dffun5  6578  dffun7  6593  fununi  6641  fvn0ssdmfun  7094  dff13  7275  dff14b  7291  fnssintima  7382  zfun  7756  uniex2  7758  dfom2  7889  ralxp3f  8162  frpoins3xpg  8165  frpoins3xp3g  8166  xpord2indlem  8172  xpord3inddlem  8179  soseq  8184  fimaxg  9323  fiint  9366  fiintOLD  9367  dfsup2  9484  fiming  9538  oemapso  9722  scottexs  9927  scott0s  9928  iscard2  10016  acnnum  10092  dfac9  10177  dfacacn  10182  kmlem4  10194  kmlem12  10202  axpowndlem3  10639  zfcndun  10655  zfcndpow  10656  zfcndac  10659  axgroth5  10864  axgroth6  10868  addsrmo  11113  mulsrmo  11114  infm3  12227  raluz2  12939  nnwos  12957  ralrp  13055  cotr2g  15015  lo1resb  15600  rlimresb  15601  o1resb  15602  modfsummod  15830  isprm4  16721  acsfn1  17704  acsfn2  17706  lublecllem  18405  isirred2  20421  isdomn5  20710  isdomn2OLD  20712  isdomn3  20715  isdomn4r  20719  iunocv  21699  ist1-2  23355  isnrm2  23366  dfconn2  23427  alexsubALTlem3  24057  ismbl  25561  dyadmbllem  25634  ellimc3  25914  dchrelbas2  27281  dchrelbas3  27282  eqscut2  27851  addsproplem4  28005  addsproplem6  28007  addsprop  28009  negsproplem4  28063  negsproplem6  28065  negsprop  28067  mulsprop  28156  isch2  31242  choc0  31345  h1dei  31569  mdsl2i  32341  disjorf  32592  bnj1101  34798  bnj1109  34800  bnj1533  34866  bnj580  34927  bnj864  34936  bnj865  34937  bnj978  34963  bnj1049  34988  bnj1090  34993  bnj1145  35007  fineqvpow  35110  axextprim  35701  axunprim  35703  axpowprim  35704  untuni  35709  3orit  35716  biimpexp  35717  elintfv  35765  dfon2lem8  35791  dfom5b  35913  iineq1i  36197  ixpeq1i  36201  ss-ax8  36226  rdgeqoa  37371  wl-equsalcom  37544  wl-sb9v  37550  poimirlem25  37652  poimirlem30  37657  tsim1  38137  inxpss  38312  idinxpss  38313  ref5  38314  idinxpssinxp  38318  ineleq  38355  cocossss  38437  cosscnvssid3  38477  trcoss2  38485  redundpbi1  38632  dfeldisj3  38720  dfantisymrel5  38763  antisymrelres  38764  cvlsupr3  39345  pmapglbx  39771  isltrn2N  40122  cdlemefrs29bpre0  40398  3factsumint2  42023  3factsumint3  42024  3factsumint4  42025  3factsumint  42026  aks4d1p7  42084  aks4d1p8  42088  fphpd  42827  dford4  43041  fnwe2lem2  43063  unielss  43230  safesnsupfilb  43431  faosnf0.11b  43440  ifpidg  43504  ifpid1g  43507  ifpor123g  43521  dfsucon  43536  undmrnresiss  43617  elintima  43666  df3or2  43781  dfhe3  43788  dffrege76  43952  dffrege115  43991  frege131  44007  ntrneikb  44107  ismnuprim  44313  ismnushort  44320  pm14.12  44440  dfvd2an  44602  dfvd3  44611  dfvd3an  44614  uun2221  44833  uun2221p1  44834  uun2221p2  44835  sswfaxreg  45004  modelac8prim  45009  disjinfi  45197  supxrleubrnmptf  45462  fsummulc1f  45586  fsumiunss  45590  fnlimfvre2  45692  limsupreuz  45752  dvmptmulf  45952  dvnmul  45958  dvmptfprodlem  45959  dvnprodlem2  45962  sge0ltfirpmpt2  46441  hoidmv1le  46609  hoidmvle  46615  vonioolem2  46696  smflimlem3  46788  2reu8i  47125  ichexmpl2  47457  setrec2  49214  aacllem  49320