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 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  464  imor  850  ifpnOLD  1072  eximal  1783  nfnbi  1856  19.43  1884  19.37v  1994  19.37  2224  sbrimOLD  2300  sbor  2302  sb8v  2347  sb8f  2348  dfsb3  2492  mo4f  2560  2mos  2644  neor  3033  r19.43  3121  r19.23v  3181  r3al  3195  r19.23t  3251  ceqsralt  3506  ralab  3687  ralabOLD  3688  ralrab  3689  euind  3720  reu2  3721  rmo4  3726  rmo3f  3730  rmo4f  3731  reuind  3749  2reu5lem3  3753  rmo3  3883  dfdif3  4114  raldifb  4144  elunant  4178  inssdif0  4369  ssundif  4487  dfif2  4530  pwss  4625  ralsnsg  4672  ralsng  4677  disjsn  4715  snssb  4786  snssgOLD  4788  raldifsni  4798  raldifsnb  4799  unissb  4943  unissbOLD  4944  intprg  4985  intprOLD  4987  dfiin2g  5035  disjor  5128  dftr2  5267  axrep1  5286  axrep6  5292  axpweq  5348  zfpow  5364  axpow2  5365  reusv2lem4  5399  reusv2  5401  el  5437  dffr6  5634  raliunxp  5839  cotrg  6108  cotrgOLD  6109  idrefALT  6112  cnvsym  6113  cnvsymOLD  6114  asymref2  6118  dffun2OLDOLD  6555  dffun4  6559  dffun5  6560  dffun7  6575  fununi  6623  fvn0ssdmfun  7076  dff13  7257  dff14b  7273  fnssintima  7362  zfun  7730  uniex2  7732  dfom2  7861  ralxp3f  8128  frpoins3xpg  8131  frpoins3xp3g  8132  xpord2indlem  8138  xpord3inddlem  8145  soseq  8150  fimaxg  9296  fiint  9330  dfsup2  9445  fiming  9499  oemapso  9683  scottexs  9888  scott0s  9889  iscard2  9977  acnnum  10053  dfac9  10137  dfacacn  10142  kmlem4  10154  kmlem12  10162  axpowndlem3  10600  zfcndun  10616  zfcndpow  10617  zfcndac  10620  axgroth5  10825  axgroth6  10829  addsrmo  11074  mulsrmo  11075  infm3  12180  raluz2  12888  nnwos  12906  ralrp  13001  cotr2g  14930  lo1resb  15515  rlimresb  15516  o1resb  15517  modfsummod  15747  isprm4  16628  acsfn1  17612  acsfn2  17614  lublecllem  18323  isirred2  20319  isdomn2  21204  isdomn5  21206  iunocv  21544  ist1-2  23171  isnrm2  23182  dfconn2  23243  alexsubALTlem3  23873  ismbl  25375  dyadmbllem  25448  ellimc3  25728  dchrelbas2  27083  dchrelbas3  27084  eqscut2  27652  addsproplem4  27802  addsproplem6  27804  addsprop  27806  negsproplem4  27856  negsproplem6  27858  negsprop  27860  mulsprop  27943  isch2  30909  choc0  31012  h1dei  31236  mdsl2i  32008  disjorf  32243  bnj1101  34259  bnj1109  34261  bnj1533  34327  bnj580  34388  bnj864  34397  bnj865  34398  bnj978  34424  bnj1049  34449  bnj1090  34454  bnj1145  34468  fineqvpow  34560  axextprim  35140  axunprim  35142  axpowprim  35143  untuni  35148  3orit  35155  biimpexp  35156  elintfv  35206  dfon2lem8  35232  dfom5b  35354  rdgeqoa  36715  wl-equsalcom  36875  poimirlem25  36977  poimirlem30  36982  tsim1  37462  ralin  37579  inxpss  37644  idinxpss  37645  ref5  37646  idinxpssinxp  37650  ineleq  37687  cocossss  37770  cosscnvssid3  37810  trcoss2  37818  redundpbi1  37965  dfeldisj3  38053  dfantisymrel5  38096  antisymrelres  38097  cvlsupr3  38678  pmapglbx  39104  isltrn2N  39455  cdlemefrs29bpre0  39731  3factsumint2  41354  3factsumint3  41355  3factsumint4  41356  3factsumint  41357  aks4d1p7  41415  aks4d1p8  41419  fphpd  42017  dford4  42231  fnwe2lem2  42256  isdomn3  42409  unielss  42430  safesnsupfilb  42632  faosnf0.11b  42641  ifpidg  42705  ifpid1g  42708  ifpor123g  42722  dfsucon  42737  undmrnresiss  42818  elintima  42867  df3or2  42982  dfhe3  42989  dffrege76  43153  dffrege115  43192  frege131  43208  ntrneikb  43308  ismnuprim  43516  ismnushort  43523  pm14.12  43643  dfvd2an  43806  dfvd3  43815  dfvd3an  43818  uun2221  44037  uun2221p1  44038  uun2221p2  44039  disjinfi  44350  supxrleubrnmptf  44620  fsummulc1f  44746  fsumiunss  44750  fnlimfvre2  44852  limsupreuz  44912  limsupvaluz2  44913  dvmptmulf  45112  dvnmul  45118  dvmptfprodlem  45119  dvnprodlem2  45122  sge0ltfirpmpt2  45601  hoidmv1le  45769  hoidmvle  45775  vonioolem2  45856  smflimlem3  45948  2reu8i  46280  ichexmpl2  46597  setrec2  47902  aacllem  48010