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 206

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 207

This theorem is referenced by:  ancomst  464  imor  853  3jaob  1428  eximal  1782  nfnbi  1855  19.43  1882  19.37v  1997  19.37  2233  sbor  2306  sb8v  2351  sb8f  2352  dfsb3  2492  mo4f  2560  2mos  2642  2mosOLD  2643  neor  3017  r19.43  3101  r19.23v  3161  r3al  3175  r19.23t  3233  sbralieOLD  3328  ceqsralt  3482  ralab  3664  ralrab  3665  euind  3695  reu2  3696  rmo4  3701  rmo3f  3705  rmo4f  3706  reuind  3724  2reu5lem3  3728  rmo3  3852  dfdif3OLD  4081  raldifb  4112  elunant  4147  ralin  4212  inssdif0  4337  ssundif  4451  dfif2  4490  pwss  4586  ralsnsg  4634  ralsng  4639  disjsn  4675  snssb  4746  snssgOLD  4748  raldifsni  4759  raldifsnb  4760  unissb  4903  unissbOLD  4904  intprg  4945  dfiin2g  4996  disjor  5089  dftr2  5216  axrep1  5235  axrep4v  5239  axrep4  5240  axrep6OLD  5244  axpweq  5306  zfpow  5321  axpow2  5322  reusv2lem4  5356  reusv2  5358  el  5397  dffr6  5594  raliunxp  5803  cotrg  6080  cotrgOLD  6081  idrefALT  6084  cnvsym  6085  cnvsymOLD  6086  asymref2  6090  dffun2OLDOLD  6523  dffun4  6527  dffun5  6528  dffun7  6543  fununi  6591  fvn0ssdmfun  7046  dff13  7229  dff14b  7246  fnssintima  7337  zfun  7712  uniex2  7714  dfom2  7844  ralxp3f  8116  frpoins3xpg  8119  frpoins3xp3g  8120  xpord2indlem  8126  xpord3inddlem  8133  soseq  8138  fimaxg  9234  fiint  9277  fiintOLD  9278  dfsup2  9395  fiming  9451  oemapso  9635  scottexs  9840  scott0s  9841  iscard2  9929  acnnum  10005  dfac9  10090  dfacacn  10095  kmlem4  10107  kmlem12  10115  axpowndlem3  10552  zfcndun  10568  zfcndpow  10569  zfcndac  10572  axgroth5  10777  axgroth6  10781  addsrmo  11026  mulsrmo  11027  infm3  12142  raluz2  12856  nnwos  12874  ralrp  12973  cotr2g  14942  lo1resb  15530  rlimresb  15531  o1resb  15532  modfsummod  15760  isprm4  16654  acsfn1  17622  acsfn2  17624  lublecllem  18319  isirred2  20330  isdomn5  20619  isdomn2OLD  20621  isdomn3  20624  isdomn4r  20628  iunocv  21590  ist1-2  23234  isnrm2  23245  dfconn2  23306  alexsubALTlem3  23936  ismbl  25427  dyadmbllem  25500  ellimc3  25780  dchrelbas2  27148  dchrelbas3  27149  eqscut2  27718  addsproplem4  27879  addsproplem6  27881  addsprop  27883  negsproplem4  27937  negsproplem6  27939  negsprop  27941  mulsprop  28033  onsis  28172  isch2  31152  choc0  31255  h1dei  31479  mdsl2i  32251  disjorf  32508  bnj1101  34774  bnj1109  34776  bnj1533  34842  bnj580  34903  bnj864  34912  bnj865  34913  bnj978  34939  bnj1049  34964  bnj1090  34969  bnj1145  34983  fineqvpow  35086  vonf1owev  35095  antnestALT  35681  axextprim  35688  axunprim  35690  axpowprim  35691  untuni  35696  3orit  35703  biimpexp  35704  elintfv  35752  dfon2lem8  35778  dfom5b  35900  iineq1i  36184  ixpeq1i  36188  ss-ax8  36213  rdgeqoa  37358  wl-equsalcom  37531  wl-sb9v  37537  poimirlem25  37639  poimirlem30  37644  tsim1  38124  inxpss  38299  idinxpss  38300  ref5  38301  idinxpssinxp  38305  ineleq  38336  cocossss  38427  cosscnvssid3  38467  trcoss2  38475  redundpbi1  38622  dfeldisj3  38711  dfantisymrel5  38754  antisymrelres  38755  cvlsupr3  39337  pmapglbx  39763  isltrn2N  40114  cdlemefrs29bpre0  40390  3factsumint2  42010  3factsumint3  42011  3factsumint4  42012  3factsumint  42013  aks4d1p7  42071  aks4d1p8  42075  fphpd  42804  dford4  43018  fnwe2lem2  43040  unielss  43207  safesnsupfilb  43407  faosnf0.11b  43416  ifpidg  43480  ifpid1g  43483  ifpor123g  43497  dfsucon  43512  undmrnresiss  43593  elintima  43642  df3or2  43757  dfhe3  43764  dffrege76  43928  dffrege115  43967  frege131  43983  ntrneikb  44083  ismnuprim  44283  ismnushort  44290  pm14.12  44410  dfvd2an  44572  dfvd3  44581  dfvd3an  44584  uun2221  44802  uun2221p1  44803  uun2221p2  44804  sswfaxreg  44977  modelac8prim  44982  disjinfi  45186  supxrleubrnmptf  45447  fsummulc1f  45569  fsumiunss  45573  fnlimfvre2  45675  limsupreuz  45735  dvmptmulf  45935  dvnmul  45941  dvmptfprodlem  45942  dvnprodlem2  45945  sge0ltfirpmpt2  46424  hoidmv1le  46592  hoidmvle  46598  vonioolem2  46679  smflimlem3  46771  2reu8i  47114  ichexmpl2  47471  setrec2  49684  aacllem  49790