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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ancomst  470  imor  867  3jaob  1453  eximal  1815  nfnbi  1888  19.43  1915  19.37v  2030  19.37  2268  sbor  2339  sb8v  2382  sb8f  2383  dfsb3  2523  mo4f  2592  2mos  2674  neor  3047  r19.43  3130  r19.23v  3189  r3al  3200  r19.23t  3258  sbralieOLD  3340  ceqsralt  3484  ralab  3651  ralrab  3652  euind  3682  reu2  3683  rmo4  3688  rmo3f  3692  rmo4f  3693  reuind  3711  2reu5lem3  3715  rmo3  3836  raldifb  4096  elunant  4130  ralin  4195  inssdif0OLD  4323  ssundif  4443  dfif2  4484  pwss  4581  ralsnsg  4631  ralsng  4636  disjsn  4672  snssb  4743  raldifsni  4758  raldifsnb  4759  unissb  4901  intprg  4941  dfiin2g  4989  iunssf  5001  iunss  5003  disjor  5085  dftr2  5214  axrep1  5233  axrep4v  5237  axrep4  5238  axrep6OLD  5242  axpweq  5315  zfpow  5331  axpow2  5332  reusv2lem4  5366  reusv2  5368  el.OLD  5414  dffr6  5611  raliunxp  5819  cotrg  6105  idrefALT  6107  cnvsym  6108  asymref2  6111  dffun4  6546  dffun5  6547  dffun7  6560  fununi  6608  fvn0ssdmfun  7067  dff13  7251  dff14b  7268  fnssintima  7365  zfun  7737  uniex2OLD  7740  dfom2  7864  ralxp3f  8135  frpoins3xpg  8138  frpoins3xp3g  8139  xpord2indlem  8145  xpord3inddlem  8152  soseq  8157  fimaxg  9257  fiint  9296  dfsup2  9414  fiming  9470  oemapso  9661  scottexsOLD  9882  scott0bsOLD  9884  iscard2  9981  acnnum  10055  dfac9  10139  dfacacn  10144  kmlem4  10156  kmlem12  10164  axpowndlem3  10608  zfcndun  10624  zfcndpow  10625  zfcndac  10628  axgroth5  10833  axgroth6  10837  addsrmo  11082  mulsrmo  11083  infm3  12198  raluz2  12946  nnwos  12964  ralrp  13064  cotr2g  15049  lo1resb  15651  rlimresb  15652  o1resb  15653  modfsummod  15881  isprm4  16774  acsfn1  17749  acsfn2  17751  lublecllem  18446  isirred2  20562  isdomn5  20872  isdomn3  20876  isdomn4r  20880  iunocv  21894  ist1-2  23572  isnrm2  23583  dfconn2  23644  alexsubALTlem3  24275  ismbl  25754  dyadmbllem  25827  ellimc3  26106  dchrelbas2  27473  dchrelbas3  27474  eqcuts2  28051  addsproplem4  28237  addsproplem6  28239  addsprop  28241  negsproplem4  28296  negsproplem6  28298  negsprop  28300  mulsprop  28395  onsis  28539  ons2ind  28540  isch2  31704  choc0  31807  h1dei  32031  mdsl2i  32803  disjorf  33052  bnj1101  35294  bnj1109  35296  bnj1533  35361  bnj580  35422  bnj864  35431  bnj865  35432  bnj978  35458  bnj1049  35483  bnj1090  35488  bnj1145  35502  fineqvpow  35641  axpowg  35672  vonf1wev  35705  vonf1owevOLD  35707  antnestALT  36273  axextprim  36280  axunprim  36282  axpowprim  36283  untuni  36288  3orit  36295  biimpexp  36296  elintfv  36344  dfon2lem8  36367  dfom5b  36489  iineq1i  36816  ixpeq1i  36820  ss-ax8  36845  mh-regprimbi  37164  mh-infprim2bi  37166  rdgeqoa  38124  wl-equsalcom  38306  wl-sb9v  38312  poimirlem25  38394  poimirlem30  38399  tsim1  38878  inxpss  39065  idinxpss  39066  ref5  39067  idinxpssinxp  39071  ineleq  39102  cocossss  39274  cosscnvssid3  39314  trcoss2  39322  redundpbi1  39463  dfeldisj3  39559  qmapeldisjsim  39608  dfantisymrel5  39613  antisymrelres  39614  cvlsupr3  40217  pmapglbx  40642  isltrn2N  40993  cdlemefrs29bpre0  41269  3factsumint2  42888  3factsumint3  42889  3factsumint4  42890  3factsumint  42891  aks4d1p7  42949  aks4d1p8  42953  fphpd  43657  dford4  43870  fnwe2lem2  43892  unielss  44059  safesnsupfilb  44258  faosnf0.11b  44267  ifpidg  44331  ifpid1g  44334  ifpor123g  44348  dfsucon  44363  undmrnresiss  44444  elintima  44493  df3or2  44608  dfhe3  44615  dffrege76  44779  dffrege115  44818  frege131  44834  ntrneikb  44934  ismnuprim  45118  ismnushort  45125  pm14.12  45245  dfvd2an  45405  dfvd3  45414  dfvd3an  45417  uun2221  45635  uun2221p1  45636  uun2221p2  45637  sswfaxreg  45810  modelac8prim  45815  disjinfi  46024  supxrleubrnmptf  46279  fsummulc1f  46401  fsumiunss  46405  fnlimfvre2  46505  limsupreuz  46565  dvmptmulf  46765  dvnmul  46771  dvmptfprodlem  46772  dvnprodlem2  46775  sge0ltfirpmpt2  47254  hoidmv1le  47422  hoidmvle  47428  vonioolem2  47509  smflimlem3  47601  2reu8i  48001  ichexmpl2  48370  setrec2  50621  aacllem  50772