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  852  3jaob  1426  eximal  1780  nfnbi  1853  19.43  1881  19.37v  1991  19.37  2233  sbrimOLD  2309  sbor  2311  sb8v  2358  sb8f  2359  dfsb3  2502  mo4f  2570  2mos  2652  2mosOLD  2653  neor  3040  r19.43  3128  r19.23v  3189  r3al  3203  r19.23t  3261  sbralie  3366  ceqsralt  3524  ralab  3713  ralabOLD  3714  ralrab  3715  euind  3746  reu2  3747  rmo4  3752  rmo3f  3756  rmo4f  3757  reuind  3775  2reu5lem3  3779  rmo3  3911  dfdif3OLD  4141  raldifb  4172  elunant  4207  inssdif0  4397  ssundif  4511  dfif2  4550  pwss  4645  ralsnsg  4692  ralsng  4697  disjsn  4736  snssb  4807  snssgOLD  4809  raldifsni  4820  raldifsnb  4821  unissb  4963  unissbOLD  4964  intprg  5005  dfiin2g  5055  disjor  5148  dftr2  5285  axrep1  5304  axrep6  5310  axpweq  5369  zfpow  5384  axpow2  5385  reusv2lem4  5419  reusv2  5421  el  5457  dffr6  5655  raliunxp  5864  cotrg  6139  cotrgOLD  6140  idrefALT  6143  cnvsym  6144  cnvsymOLD  6145  asymref2  6149  dffun2OLDOLD  6585  dffun4  6589  dffun5  6590  dffun7  6605  fununi  6653  fvn0ssdmfun  7108  dff13  7292  dff14b  7308  fnssintima  7398  zfun  7771  uniex2  7773  dfom2  7905  ralxp3f  8178  frpoins3xpg  8181  frpoins3xp3g  8182  xpord2indlem  8188  xpord3inddlem  8195  soseq  8200  fimaxg  9351  fiint  9394  fiintOLD  9395  dfsup2  9513  fiming  9567  oemapso  9751  scottexs  9956  scott0s  9957  iscard2  10045  acnnum  10121  dfac9  10206  dfacacn  10211  kmlem4  10223  kmlem12  10231  axpowndlem3  10668  zfcndun  10684  zfcndpow  10685  zfcndac  10688  axgroth5  10893  axgroth6  10897  addsrmo  11142  mulsrmo  11143  infm3  12254  raluz2  12962  nnwos  12980  ralrp  13077  cotr2g  15025  lo1resb  15610  rlimresb  15611  o1resb  15612  modfsummod  15842  isprm4  16731  acsfn1  17719  acsfn2  17721  lublecllem  18430  isirred2  20447  isdomn5  20732  isdomn2OLD  20734  isdomn3  20737  isdomn4r  20741  iunocv  21722  ist1-2  23376  isnrm2  23387  dfconn2  23448  alexsubALTlem3  24078  ismbl  25580  dyadmbllem  25653  ellimc3  25934  dchrelbas2  27299  dchrelbas3  27300  eqscut2  27869  addsproplem4  28023  addsproplem6  28025  addsprop  28027  negsproplem4  28081  negsproplem6  28083  negsprop  28085  mulsprop  28174  isch2  31255  choc0  31358  h1dei  31582  mdsl2i  32354  disjorf  32601  bnj1101  34760  bnj1109  34762  bnj1533  34828  bnj580  34889  bnj864  34898  bnj865  34899  bnj978  34925  bnj1049  34950  bnj1090  34955  bnj1145  34969  fineqvpow  35072  axextprim  35663  axunprim  35665  axpowprim  35666  untuni  35671  3orit  35678  biimpexp  35679  elintfv  35728  dfon2lem8  35754  dfom5b  35876  iineq1i  36160  ixpeq1i  36164  ss-ax8  36191  rdgeqoa  37336  wl-equsalcom  37497  wl-sb9v  37503  poimirlem25  37605  poimirlem30  37610  tsim1  38090  ralin  38204  inxpss  38267  idinxpss  38268  ref5  38269  idinxpssinxp  38273  ineleq  38310  cocossss  38392  cosscnvssid3  38432  trcoss2  38440  redundpbi1  38587  dfeldisj3  38675  dfantisymrel5  38718  antisymrelres  38719  cvlsupr3  39300  pmapglbx  39726  isltrn2N  40077  cdlemefrs29bpre0  40353  3factsumint2  41979  3factsumint3  41980  3factsumint4  41981  3factsumint  41982  aks4d1p7  42040  aks4d1p8  42044  fphpd  42772  dford4  42986  fnwe2lem2  43008  unielss  43179  safesnsupfilb  43380  faosnf0.11b  43389  ifpidg  43453  ifpid1g  43456  ifpor123g  43470  dfsucon  43485  undmrnresiss  43566  elintima  43615  df3or2  43730  dfhe3  43737  dffrege76  43901  dffrege115  43940  frege131  43956  ntrneikb  44056  ismnuprim  44263  ismnushort  44270  pm14.12  44390  dfvd2an  44553  dfvd3  44562  dfvd3an  44565  uun2221  44784  uun2221p1  44785  uun2221p2  44786  disjinfi  45099  supxrleubrnmptf  45366  fsummulc1f  45492  fsumiunss  45496  fnlimfvre2  45598  limsupreuz  45658  limsupvaluz2  45659  dvmptmulf  45858  dvnmul  45864  dvmptfprodlem  45865  dvnprodlem2  45868  sge0ltfirpmpt2  46347  hoidmv1le  46515  hoidmvle  46521  vonioolem2  46602  smflimlem3  46694  2reu8i  47028  ichexmpl2  47344  setrec2  48787  aacllem  48895