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  1991  19.37  2232  sbrimOLD  2305  sbor  2307  sb8v  2354  sb8f  2355  dfsb3  2498  mo4f  2566  2mos  2648  2mosOLD  2649  neor  3024  r19.43  3108  r19.23v  3168  r3al  3182  r19.23t  3238  sbralie  3337  ceqsralt  3495  ralab  3676  ralrab  3677  euind  3707  reu2  3708  rmo4  3713  rmo3f  3717  rmo4f  3718  reuind  3736  2reu5lem3  3740  rmo3  3864  dfdif3OLD  4093  raldifb  4124  elunant  4159  ralin  4224  inssdif0  4349  ssundif  4463  dfif2  4502  pwss  4598  ralsnsg  4646  ralsng  4651  disjsn  4687  snssb  4758  snssgOLD  4760  raldifsni  4771  raldifsnb  4772  unissb  4915  unissbOLD  4916  intprg  4957  dfiin2g  5008  disjor  5101  dftr2  5231  axrep1  5250  axrep4v  5254  axrep4  5255  axrep6OLD  5259  axpweq  5321  zfpow  5336  axpow2  5337  reusv2lem4  5371  reusv2  5373  el  5412  dffr6  5609  raliunxp  5819  cotrg  6096  cotrgOLD  6097  idrefALT  6100  cnvsym  6101  cnvsymOLD  6102  asymref2  6106  dffun2OLDOLD  6542  dffun4  6546  dffun5  6547  dffun7  6562  fununi  6610  fvn0ssdmfun  7063  dff13  7246  dff14b  7263  fnssintima  7354  zfun  7728  uniex2  7730  dfom2  7861  ralxp3f  8134  frpoins3xpg  8137  frpoins3xp3g  8138  xpord2indlem  8144  xpord3inddlem  8151  soseq  8156  fimaxg  9293  fiint  9336  fiintOLD  9337  dfsup2  9454  fiming  9510  oemapso  9694  scottexs  9899  scott0s  9900  iscard2  9988  acnnum  10064  dfac9  10149  dfacacn  10154  kmlem4  10166  kmlem12  10174  axpowndlem3  10611  zfcndun  10627  zfcndpow  10628  zfcndac  10631  axgroth5  10836  axgroth6  10840  addsrmo  11085  mulsrmo  11086  infm3  12199  raluz2  12911  nnwos  12929  ralrp  13027  cotr2g  14993  lo1resb  15578  rlimresb  15579  o1resb  15580  modfsummod  15808  isprm4  16701  acsfn1  17671  acsfn2  17673  lublecllem  18368  isirred2  20379  isdomn5  20668  isdomn2OLD  20670  isdomn3  20673  isdomn4r  20677  iunocv  21639  ist1-2  23283  isnrm2  23294  dfconn2  23355  alexsubALTlem3  23985  ismbl  25477  dyadmbllem  25550  ellimc3  25830  dchrelbas2  27198  dchrelbas3  27199  eqscut2  27768  addsproplem4  27922  addsproplem6  27924  addsprop  27926  negsproplem4  27980  negsproplem6  27982  negsprop  27984  mulsprop  28073  isch2  31150  choc0  31253  h1dei  31477  mdsl2i  32249  disjorf  32506  bnj1101  34761  bnj1109  34763  bnj1533  34829  bnj580  34890  bnj864  34899  bnj865  34900  bnj978  34926  bnj1049  34951  bnj1090  34956  bnj1145  34970  fineqvpow  35073  axextprim  35664  axunprim  35666  axpowprim  35667  untuni  35672  3orit  35679  biimpexp  35680  elintfv  35728  dfon2lem8  35754  dfom5b  35876  iineq1i  36160  ixpeq1i  36164  ss-ax8  36189  rdgeqoa  37334  wl-equsalcom  37507  wl-sb9v  37513  poimirlem25  37615  poimirlem30  37620  tsim1  38100  inxpss  38275  idinxpss  38276  ref5  38277  idinxpssinxp  38281  ineleq  38318  cocossss  38400  cosscnvssid3  38440  trcoss2  38448  redundpbi1  38595  dfeldisj3  38683  dfantisymrel5  38726  antisymrelres  38727  cvlsupr3  39308  pmapglbx  39734  isltrn2N  40085  cdlemefrs29bpre0  40361  3factsumint2  41981  3factsumint3  41982  3factsumint4  41983  3factsumint  41984  aks4d1p7  42042  aks4d1p8  42046  fphpd  42786  dford4  43000  fnwe2lem2  43022  unielss  43189  safesnsupfilb  43389  faosnf0.11b  43398  ifpidg  43462  ifpid1g  43465  ifpor123g  43479  dfsucon  43494  undmrnresiss  43575  elintima  43624  df3or2  43739  dfhe3  43746  dffrege76  43910  dffrege115  43949  frege131  43965  ntrneikb  44065  ismnuprim  44266  ismnushort  44273  pm14.12  44393  dfvd2an  44555  dfvd3  44564  dfvd3an  44567  uun2221  44785  uun2221p1  44786  uun2221p2  44787  sswfaxreg  44960  modelac8prim  44965  disjinfi  45164  supxrleubrnmptf  45426  fsummulc1f  45548  fsumiunss  45552  fnlimfvre2  45654  limsupreuz  45714  dvmptmulf  45914  dvnmul  45920  dvmptfprodlem  45921  dvnprodlem2  45924  sge0ltfirpmpt2  46403  hoidmv1le  46571  hoidmvle  46577  vonioolem2  46658  smflimlem3  46750  2reu8i  47090  ichexmpl2  47432  setrec2  49507  aacllem  49613