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  1783  nfnbi  1856  19.43  1883  19.37v  1998  19.37  2237  sbor  2310  sb8v  2355  sb8f  2356  dfsb3  2496  mo4f  2564  2mos  2646  2mosOLD  2647  neor  3021  r19.43  3101  r19.23v  3160  r3al  3171  r19.23t  3229  sbralieOLD  3321  ceqsralt  3472  ralab  3648  ralrab  3649  euind  3679  reu2  3680  rmo4  3685  rmo3f  3689  rmo4f  3690  reuind  3708  2reu5lem3  3712  rmo3  3836  dfdif3OLD  4067  raldifb  4098  elunant  4133  ralin  4198  inssdif0  4323  ssundif  4437  dfif2  4478  pwss  4574  ralsnsg  4624  ralsng  4629  disjsn  4665  snssb  4736  raldifsni  4748  raldifsnb  4749  unissb  4893  intprg  4933  dfiin2g  4983  iunssf  4995  iunss  4997  disjor  5077  dftr2  5204  axrep1  5222  axrep4v  5226  axrep4  5227  axrep6OLD  5231  axpweq  5293  zfpow  5308  axpow2  5309  reusv2lem4  5343  reusv2  5345  el  5384  dffr6  5577  raliunxp  5785  cotrg  6065  idrefALT  6067  cnvsym  6068  asymref2  6071  dffun4  6502  dffun5  6503  dffun7  6516  fununi  6564  fvn0ssdmfun  7016  dff13  7197  dff14b  7214  fnssintima  7305  zfun  7678  uniex2  7680  dfom2  7807  ralxp3f  8076  frpoins3xpg  8079  frpoins3xp3g  8080  xpord2indlem  8086  xpord3inddlem  8093  soseq  8098  fimaxg  9182  fiint  9222  dfsup2  9339  fiming  9395  oemapso  9583  scottexs  9791  scott0s  9792  iscard2  9880  acnnum  9954  dfac9  10039  dfacacn  10044  kmlem4  10056  kmlem12  10064  axpowndlem3  10501  zfcndun  10517  zfcndpow  10518  zfcndac  10521  axgroth5  10726  axgroth6  10730  addsrmo  10975  mulsrmo  10976  infm3  12092  raluz2  12801  nnwos  12819  ralrp  12918  cotr2g  14890  lo1resb  15478  rlimresb  15479  o1resb  15480  modfsummod  15708  isprm4  16602  acsfn1  17575  acsfn2  17577  lublecllem  18272  isirred2  20348  isdomn5  20634  isdomn2OLD  20636  isdomn3  20639  isdomn4r  20643  iunocv  21627  ist1-2  23282  isnrm2  23293  dfconn2  23354  alexsubALTlem3  23984  ismbl  25474  dyadmbllem  25547  ellimc3  25827  dchrelbas2  27195  dchrelbas3  27196  eqscut2  27767  addsproplem4  27935  addsproplem6  27937  addsprop  27939  negsproplem4  27993  negsproplem6  27995  negsprop  27997  mulsprop  28089  onsis  28228  isch2  31224  choc0  31327  h1dei  31551  mdsl2i  32323  disjorf  32580  bnj1101  34868  bnj1109  34870  bnj1533  34936  bnj580  34997  bnj864  35006  bnj865  35007  bnj978  35033  bnj1049  35058  bnj1090  35063  bnj1145  35077  fineqvpow  35210  vonf1owev  35224  antnestALT  35810  axextprim  35817  axunprim  35819  axpowprim  35820  untuni  35825  3orit  35832  biimpexp  35833  elintfv  35881  dfon2lem8  35904  dfom5b  36026  iineq1i  36312  ixpeq1i  36316  ss-ax8  36341  bj-df-sb  36769  rdgeqoa  37487  wl-equsalcom  37660  wl-sb9v  37666  poimirlem25  37758  poimirlem30  37763  tsim1  38243  inxpss  38422  idinxpss  38423  ref5  38424  idinxpssinxp  38428  ineleq  38459  cocossss  38611  cosscnvssid3  38651  trcoss2  38659  redundpbi1  38800  dfeldisj3  38890  dfantisymrel5  38933  antisymrelres  38934  cvlsupr3  39516  pmapglbx  39941  isltrn2N  40292  cdlemefrs29bpre0  40568  3factsumint2  42188  3factsumint3  42189  3factsumint4  42190  3factsumint  42191  aks4d1p7  42249  aks4d1p8  42253  fphpd  42973  dford4  43186  fnwe2lem2  43208  unielss  43375  safesnsupfilb  43575  faosnf0.11b  43584  ifpidg  43648  ifpid1g  43651  ifpor123g  43665  dfsucon  43680  undmrnresiss  43761  elintima  43810  df3or2  43925  dfhe3  43932  dffrege76  44096  dffrege115  44135  frege131  44151  ntrneikb  44251  ismnuprim  44451  ismnushort  44458  pm14.12  44578  dfvd2an  44739  dfvd3  44748  dfvd3an  44751  uun2221  44969  uun2221p1  44970  uun2221p2  44971  sswfaxreg  45144  modelac8prim  45149  disjinfi  45352  supxrleubrnmptf  45611  fsummulc1f  45733  fsumiunss  45737  fnlimfvre2  45837  limsupreuz  45897  dvmptmulf  46097  dvnmul  46103  dvmptfprodlem  46104  dvnprodlem2  46107  sge0ltfirpmpt2  46586  hoidmv1le  46754  hoidmvle  46760  vonioolem2  46841  smflimlem3  46933  2reu8i  47275  ichexmpl2  47632  setrec2  49856  aacllem  49962