Theorem imbi1i 348

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  ancomst  463  imor  849  ifpnOLD  1071  eximal  1782  nfnbi  1855  19.43  1883  19.37v  1993  19.37  2223  sbrimOLD  2299  sbor  2301  sb8v  2346  sb8f  2347  dfsb3  2491  mo4f  2559  2mos  2643  neor  3032  r19.43  3120  r19.23v  3180  r3al  3194  r19.23t  3250  ceqsralt  3505  ralab  3688  ralabOLD  3689  ralrab  3690  euind  3721  reu2  3722  rmo4  3727  rmo3f  3731  rmo4f  3732  reuind  3750  2reu5lem3  3754  rmo3  3884  dfdif3  4115  raldifb  4145  elunant  4179  inssdif0  4370  ssundif  4488  dfif2  4531  pwss  4626  ralsnsg  4673  ralsng  4678  disjsn  4716  snssb  4787  snssgOLD  4789  raldifsni  4799  raldifsnb  4800  unissb  4944  unissbOLD  4945  intprg  4986  intprOLD  4988  dfiin2g  5036  disjor  5129  dftr2  5268  axrep1  5287  axrep6  5293  axpweq  5349  zfpow  5365  axpow2  5366  reusv2lem4  5400  reusv2  5402  el  5438  dffr6  5635  raliunxp  5840  cotrg  6109  cotrgOLD  6110  idrefALT  6113  cnvsym  6114  cnvsymOLD  6115  asymref2  6119  dffun2OLDOLD  6556  dffun4  6560  dffun5  6561  dffun7  6576  fununi  6624  fvn0ssdmfun  7077  dff13  7258  dff14b  7274  fnssintima  7363  zfun  7730  uniex2  7732  dfom2  7861  ralxp3f  8127  frpoins3xpg  8130  frpoins3xp3g  8131  xpord2indlem  8137  xpord3inddlem  8144  soseq  8149  fimaxg  9294  fiint  9328  dfsup2  9443  fiming  9497  oemapso  9681  scottexs  9886  scott0s  9887  iscard2  9975  acnnum  10051  dfac9  10135  dfacacn  10140  kmlem4  10152  kmlem12  10160  axpowndlem3  10598  zfcndun  10614  zfcndpow  10615  zfcndac  10618  axgroth5  10823  axgroth6  10827  addsrmo  11072  mulsrmo  11073  infm3  12179  raluz2  12887  nnwos  12905  ralrp  13000  cotr2g  14929  lo1resb  15514  rlimresb  15515  o1resb  15516  modfsummod  15746  isprm4  16627  acsfn1  17611  acsfn2  17613  lublecllem  18319  isirred2  20314  isdomn2  21117  isdomn5  21119  iunocv  21455  ist1-2  23073  isnrm2  23084  dfconn2  23145  alexsubALTlem3  23775  ismbl  25277  dyadmbllem  25350  ellimc3  25630  dchrelbas2  26974  dchrelbas3  26975  eqscut2  27542  addsproplem4  27692  addsproplem6  27694  addsprop  27696  negsproplem4  27742  negsproplem6  27744  negsprop  27746  mulsprop  27823  isch2  30741  choc0  30844  h1dei  31068  mdsl2i  31840  disjorf  32075  bnj1101  34091  bnj1109  34093  bnj1533  34159  bnj580  34220  bnj864  34229  bnj865  34230  bnj978  34256  bnj1049  34281  bnj1090  34286  bnj1145  34300  fineqvpow  34392  axextprim  34972  axunprim  34974  axpowprim  34975  untuni  34980  3orit  34987  biimpexp  34988  elintfv  35038  dfon2lem8  35064  dfom5b  35186  rdgeqoa  36556  wl-equsalcom  36716  poimirlem25  36818  poimirlem30  36823  tsim1  37303  ralin  37420  inxpss  37485  idinxpss  37486  ref5  37487  idinxpssinxp  37491  ineleq  37528  cocossss  37611  cosscnvssid3  37651  trcoss2  37659  redundpbi1  37806  dfeldisj3  37894  dfantisymrel5  37937  antisymrelres  37938  cvlsupr3  38519  pmapglbx  38945  isltrn2N  39296  cdlemefrs29bpre0  39572  3factsumint2  41195  3factsumint3  41196  3factsumint4  41197  3factsumint  41198  aks4d1p7  41256  aks4d1p8  41260  fphpd  41858  dford4  42072  fnwe2lem2  42097  isdomn3  42250  unielss  42271  safesnsupfilb  42473  faosnf0.11b  42482  ifpidg  42546  ifpid1g  42549  ifpor123g  42563  dfsucon  42578  undmrnresiss  42659  elintima  42708  df3or2  42823  dfhe3  42830  dffrege76  42994  dffrege115  43033  frege131  43049  ntrneikb  43149  ismnuprim  43357  ismnushort  43364  pm14.12  43484  dfvd2an  43647  dfvd3  43656  dfvd3an  43659  uun2221  43878  uun2221p1  43879  uun2221p2  43880  disjinfi  44191  supxrleubrnmptf  44461  fsummulc1f  44587  fsumiunss  44591  fnlimfvre2  44693  limsupreuz  44753  limsupvaluz2  44754  dvmptmulf  44953  dvnmul  44959  dvmptfprodlem  44960  dvnprodlem2  44963  sge0ltfirpmpt2  45442  hoidmv1le  45610  hoidmvle  45616  vonioolem2  45697  smflimlem3  45789  2reu8i  46121  ichexmpl2  46438  setrec2  47829  aacllem  47937