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  2271  sbor  2343  sb8v  2387  sb8f  2388  dfsb3  2528  mo4f  2597  2mos  2679  neor  3052  r19.43  3135  r19.23v  3194  r3al  3205  r19.23t  3263  sbralieOLD  3346  ceqsralt  3491  ralab  3658  ralrab  3659  euind  3689  reu2  3690  rmo4  3695  rmo3f  3699  rmo4f  3700  reuind  3718  2reu5lem3  3722  rmo3  3843  raldifb  4103  elunant  4137  ralin  4202  inssdif0OLD  4330  ssundif  4450  dfif2  4491  pwss  4588  ralsnsg  4638  ralsng  4643  disjsn  4679  snssb  4750  raldifsni  4765  raldifsnb  4766  unissb  4908  intprg  4948  dfiin2g  4997  iunssf  5009  iunss  5011  disjor  5093  dftr2  5222  axrep1  5241  axrep4v  5245  axrep4  5246  axrep6OLD  5250  axpweq  5323  zfpow  5339  axpow2  5340  reusv2lem4  5374  reusv2  5376  el.OLD  5422  dffr6  5619  raliunxp  5827  cotrg  6113  idrefALT  6115  cnvsym  6116  asymref2  6119  dffun4  6553  dffun5  6554  dffun7  6567  fununi  6615  fvn0ssdmfun  7073  dff13  7254  dff14b  7271  fnssintima  7368  zfun  7739  uniex2OLD  7742  dfom2  7866  ralxp3f  8135  frpoins3xpg  8138  frpoins3xp3g  8139  xpord2indlem  8145  xpord3inddlem  8152  soseq  8157  fimaxg  9250  fiint  9289  dfsup2  9407  fiming  9463  oemapso  9654  scottexsOLD  9875  scott0bsOLD  9877  iscard2  9974  acnnum  10048  dfac9  10132  dfacacn  10137  kmlem4  10149  kmlem12  10157  axpowndlem3  10595  zfcndun  10611  zfcndpow  10612  zfcndac  10615  axgroth5  10820  axgroth6  10824  addsrmo  11069  mulsrmo  11070  infm3  12185  raluz2  12933  nnwos  12951  ralrp  13050  cotr2g  15033  lo1resb  15635  rlimresb  15636  o1resb  15637  modfsummod  15865  isprm4  16760  acsfn1  17735  acsfn2  17737  lublecllem  18432  isirred2  20529  isdomn5  20839  isdomn3  20843  isdomn4r  20847  iunocv  21861  ist1-2  23534  isnrm2  23545  dfconn2  23606  alexsubALTlem3  24237  ismbl  25716  dyadmbllem  25789  ellimc3  26069  dchrelbas2  27432  dchrelbas3  27433  eqcuts2  28010  addsproplem4  28196  addsproplem6  28198  addsprop  28200  negsproplem4  28255  negsproplem6  28257  negsprop  28259  mulsprop  28354  onsis  28498  ons2ind  28499  isch2  31622  choc0  31725  h1dei  31949  mdsl2i  32721  disjorf  32971  bnj1101  35214  bnj1109  35216  bnj1533  35281  bnj580  35342  bnj864  35351  bnj865  35352  bnj978  35378  bnj1049  35403  bnj1090  35408  bnj1145  35422  fineqvpow  35561  axpowg  35592  vonf1wev  35625  vonf1owevOLD  35627  antnestALT  36199  axextprim  36206  axunprim  36208  axpowprim  36209  untuni  36214  3orit  36221  biimpexp  36222  elintfv  36270  dfon2lem8  36293  dfom5b  36415  iineq1i  36741  ixpeq1i  36745  ss-ax8  36770  mh-regprimbi  37089  mh-infprim2bi  37091  rdgeqoa  38049  wl-equsalcom  38231  wl-sb9v  38237  poimirlem25  38329  poimirlem30  38334  tsim1  38812  inxpss  38999  idinxpss  39000  ref5  39001  idinxpssinxp  39005  ineleq  39036  cocossss  39208  cosscnvssid3  39248  trcoss2  39256  redundpbi1  39397  dfeldisj3  39493  qmapeldisjsim  39542  dfantisymrel5  39547  antisymrelres  39548  cvlsupr3  40151  pmapglbx  40576  isltrn2N  40927  cdlemefrs29bpre0  41203  3factsumint2  42822  3factsumint3  42823  3factsumint4  42824  3factsumint  42825  aks4d1p7  42883  aks4d1p8  42887  fphpd  43576  dford4  43789  fnwe2lem2  43811  unielss  43978  safesnsupfilb  44177  faosnf0.11b  44186  ifpidg  44250  ifpid1g  44253  ifpor123g  44267  dfsucon  44282  undmrnresiss  44363  elintima  44412  df3or2  44527  dfhe3  44534  dffrege76  44698  dffrege115  44737  frege131  44753  ntrneikb  44853  ismnuprim  45037  ismnushort  45044  pm14.12  45164  dfvd2an  45324  dfvd3  45333  dfvd3an  45336  uun2221  45554  uun2221p1  45555  uun2221p2  45556  sswfaxreg  45729  modelac8prim  45734  disjinfi  45943  supxrleubrnmptf  46198  fsummulc1f  46320  fsumiunss  46324  fnlimfvre2  46424  limsupreuz  46484  dvmptmulf  46684  dvnmul  46690  dvmptfprodlem  46691  dvnprodlem2  46694  sge0ltfirpmpt2  47173  hoidmv1le  47341  hoidmvle  47347  vonioolem2  47428  smflimlem3  47520  2reu8i  47883  ichexmpl2  48252  setrec2  50506  aacllem  50654