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  2235  sbor  2308  sb8v  2353  sb8f  2354  dfsb3  2494  mo4f  2562  2mos  2644  2mosOLD  2645  neor  3020  r19.43  3100  r19.23v  3159  r3al  3170  r19.23t  3228  sbralieOLD  3320  ceqsralt  3471  ralab  3647  ralrab  3648  euind  3678  reu2  3679  rmo4  3684  rmo3f  3688  rmo4f  3689  reuind  3707  2reu5lem3  3711  rmo3  3835  dfdif3OLD  4063  raldifb  4094  elunant  4129  ralin  4194  inssdif0  4319  ssundif  4433  dfif2  4472  pwss  4568  ralsnsg  4618  ralsng  4623  disjsn  4659  snssb  4730  raldifsni  4742  raldifsnb  4743  unissb  4886  intprg  4926  dfiin2g  4976  disjor  5068  dftr2  5195  axrep1  5213  axrep4v  5217  axrep4  5218  axrep6OLD  5222  axpweq  5284  zfpow  5299  axpow2  5300  reusv2lem4  5334  reusv2  5336  el  5375  dffr6  5567  raliunxp  5774  cotrg  6053  idrefALT  6055  cnvsym  6056  asymref2  6059  dffun4  6489  dffun5  6490  dffun7  6503  fununi  6551  fvn0ssdmfun  7002  dff13  7183  dff14b  7200  fnssintima  7291  zfun  7664  uniex2  7666  dfom2  7793  ralxp3f  8062  frpoins3xpg  8065  frpoins3xp3g  8066  xpord2indlem  8072  xpord3inddlem  8079  soseq  8084  fimaxg  9166  fiint  9206  dfsup2  9323  fiming  9379  oemapso  9567  scottexs  9775  scott0s  9776  iscard2  9864  acnnum  9938  dfac9  10023  dfacacn  10028  kmlem4  10040  kmlem12  10048  axpowndlem3  10485  zfcndun  10501  zfcndpow  10502  zfcndac  10505  axgroth5  10710  axgroth6  10714  addsrmo  10959  mulsrmo  10960  infm3  12076  raluz2  12790  nnwos  12808  ralrp  12907  cotr2g  14878  lo1resb  15466  rlimresb  15467  o1resb  15468  modfsummod  15696  isprm4  16590  acsfn1  17562  acsfn2  17564  lublecllem  18259  isirred2  20334  isdomn5  20620  isdomn2OLD  20622  isdomn3  20625  isdomn4r  20629  iunocv  21613  ist1-2  23257  isnrm2  23268  dfconn2  23329  alexsubALTlem3  23959  ismbl  25449  dyadmbllem  25522  ellimc3  25802  dchrelbas2  27170  dchrelbas3  27171  eqscut2  27742  addsproplem4  27910  addsproplem6  27912  addsprop  27914  negsproplem4  27968  negsproplem6  27970  negsprop  27972  mulsprop  28064  onsis  28203  isch2  31195  choc0  31298  h1dei  31522  mdsl2i  32294  disjorf  32551  bnj1101  34788  bnj1109  34790  bnj1533  34856  bnj580  34917  bnj864  34926  bnj865  34927  bnj978  34953  bnj1049  34978  bnj1090  34983  bnj1145  34997  fineqvpow  35130  vonf1owev  35144  antnestALT  35730  axextprim  35737  axunprim  35739  axpowprim  35740  untuni  35745  3orit  35752  biimpexp  35753  elintfv  35801  dfon2lem8  35824  dfom5b  35946  iineq1i  36230  ixpeq1i  36234  ss-ax8  36259  rdgeqoa  37404  wl-equsalcom  37577  wl-sb9v  37583  poimirlem25  37685  poimirlem30  37690  tsim1  38170  inxpss  38345  idinxpss  38346  ref5  38347  idinxpssinxp  38351  ineleq  38382  cocossss  38473  cosscnvssid3  38513  trcoss2  38521  redundpbi1  38668  dfeldisj3  38757  dfantisymrel5  38800  antisymrelres  38801  cvlsupr3  39383  pmapglbx  39808  isltrn2N  40159  cdlemefrs29bpre0  40435  3factsumint2  42055  3factsumint3  42056  3factsumint4  42057  3factsumint  42058  aks4d1p7  42116  aks4d1p8  42120  fphpd  42849  dford4  43062  fnwe2lem2  43084  unielss  43251  safesnsupfilb  43451  faosnf0.11b  43460  ifpidg  43524  ifpid1g  43527  ifpor123g  43541  dfsucon  43556  undmrnresiss  43637  elintima  43686  df3or2  43801  dfhe3  43808  dffrege76  43972  dffrege115  44011  frege131  44027  ntrneikb  44127  ismnuprim  44327  ismnushort  44334  pm14.12  44454  dfvd2an  44615  dfvd3  44624  dfvd3an  44627  uun2221  44845  uun2221p1  44846  uun2221p2  44847  sswfaxreg  45020  modelac8prim  45025  disjinfi  45229  supxrleubrnmptf  45489  fsummulc1f  45611  fsumiunss  45615  fnlimfvre2  45715  limsupreuz  45775  dvmptmulf  45975  dvnmul  45981  dvmptfprodlem  45982  dvnprodlem2  45985  sge0ltfirpmpt2  46464  hoidmv1le  46632  hoidmvle  46638  vonioolem2  46719  smflimlem3  46811  2reu8i  47144  ichexmpl2  47501  setrec2  49727  aacllem  49833