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  1454  eximal  1815  nfnbi  1888  19.43  1917  19.37v  2032  19.37  2272  sbor  2343  sb8v  2385  sb8f  2386  dfsb3  2526  mo4f  2595  2mos  2677  neor  3051  r19.43  3134  r19.23v  3193  r3al  3204  r19.23t  3262  sbralieOLD  3344  ceqsralt  3488  ralab  3654  ralrab  3655  euind  3685  reu2  3686  rmo4  3691  rmo3f  3695  rmo4f  3696  reuind  3714  2reu5lem3  3718  rmo3  3840  raldifb  4088  ralin  4149  elunant  4185  inssdif0OLD  4326  ssundif  4446  dfif2  4487  pwss  4585  ralsnsg  4632  ralsng  4637  disjsn  4673  snssb  4745  raldifsni  4760  raldifsnb  4761  unissb  4906  intprg  4946  dfiin2g  4994  iunssf  5006  iunss  5008  disjor  5090  dftr2  5220  axrep1  5239  axrep4v  5243  axrep4  5244  axpweq  5319  zfpow  5335  axpow2  5336  reusv2lem4  5370  reusv2  5372  el.OLD  5414  dffr6  5614  raliunxp  5826  cotrg  6123  idrefALT  6125  cnvsym  6126  asymref2  6129  dffun4  6579  dffun5  6580  dffun7  6595  fununi  6645  fvn0ssdmfun  7106  dff13  7289  dff14b  7306  fnssintima  7403  zfun  7784  uniex2OLD  7787  dfom2  7913  ovmptss  8139  fnwe2lem3  8184  ralxp3f  8191  frpoins3xpg  8194  frpoins3xp3g  8195  xpord2indlem  8201  xpord3inddlem  8208  soseq  8213  fimaxg  9316  fiint  9356  dfsup2  9473  fiming  9529  oemapso  9720  scottexsOLD  9980  scott0bsOLD  9982  setrec2  10014  iscard2  10094  acnnum  10170  dfac9  10254  dfacacn  10259  kmlem4  10271  kmlem12  10279  axpowndlem3  10723  zfcndun  10739  zfcndpow  10740  zfcndac  10743  axgroth5  10948  axgroth6  10952  addsrmo  11197  mulsrmo  11198  infm3  12316  raluz2  13064  nnwos  13082  ralrp  13182  cotr2g  15172  lo1resb  15775  rlimresb  15776  o1resb  15777  modfsummod  16005  isprm4  16903  acsfn1  17885  acsfn2  17887  lublecllem  18582  isirred2  20702  isdomn5  21013  isdomn3  21017  isdomn4r  21021  iunocv  22042  ist1-2  23720  isnrm2  23731  dfconn2  23792  alexsubALTlem3  24423  ismbl  25902  dyadmbllem  25975  ellimc3  26254  dchrelbas2  27621  dchrelbas3  27622  eqcuts2  28229  addsproplem4  28415  addsproplem6  28417  addsprop  28419  negsproplem4  28474  negsproplem6  28476  negsprop  28478  mulsprop  28573  onsis  28717  ons2ind  28718  isch2  31882  choc0  31985  h1dei  32209  mdsl2i  32981  disjorf  33271  bnj1101  35526  bnj1109  35528  bnj1533  35593  bnj580  35654  bnj864  35663  bnj865  35664  bnj978  35690  bnj1049  35715  bnj1090  35720  bnj1145  35734  rmo6  35821  fineqvpow  35924  axpowg  35955  vonf1wev  36077  vonf1owevOLD  36079  antnestALT  36667  axextprim  36681  axunprim  36683  axpowprim  36684  untuni  36689  3orit  36696  biimpexp  36697  elintfv  36745  dfon2lem8  36767  dfom5b  36889  iineq1i  37200  ixpeq1i  37204  ss-ax8  37229  mh-regprimbi  37548  mh-infprim2bi  37550  cocnv1ss  38210  cocnv2ss  38213  rdgeqoa  38561  wl-equsalcom  38743  wl-sb9v  38749  poimirlem25  38831  poimirlem30  38836  tsim1  39328  inxpss  39515  idinxpss  39516  ref5  39517  idinxpssinxp  39521  ineleq  39552  cocossss  39724  cosscnvssid3  39764  trcoss2  39772  redundpbi1  39913  dfeldisj3  40009  qmapeldisjsim  40058  dfantisymrel5  40063  antisymrelres  40064  cvlsupr3  40667  pmapglbx  41092  isltrn2N  41443  cdlemefrs29bpre0  41719  3factsumint2  43338  3factsumint3  43339  3factsumint4  43340  3factsumint  43341  aks4d1p7  43399  aks4d1p8  43403  fphpd  44089  dford4  44302  unielss  44481  safesnsupfilb  44680  faosnf0.11b  44689  ifpidg  44753  ifpid1g  44756  ifpor123g  44770  dfsucon  44785  undmrnresiss  44865  elintima  44914  df3or2  45029  dfhe3  45036  dffrege76  45200  dffrege115  45239  frege131  45255  ntrneikb  45355  ismnuprim  45539  ismnushort  45546  pm14.12  45665  dfvd2an  45825  dfvd3  45834  dfvd3an  45837  uun2221  46055  uun2221p1  46056  uun2221p2  46057  sswfaxreg  46241  modelac8prim  46246  disjinfi  46480  supxrleubrnmptf  46734  fsummulc1f  46856  fsumiunss  46860  fnlimfvre2  46960  limsupreuz  47020  dvmptmulf  47220  dvnmul  47226  dvmptfprodlem  47227  dvnprodlem2  47230  sge0ltfirpmpt2  47709  hoidmv1le  47877  hoidmvle  47883  vonioolem2  47964  smflimlem3  48056  2reu8i  48457  ichexmpl2  48825  aacllem  51367