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 205

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 206

This theorem is referenced by:  ancomst  464  imor  849  ifpnOLD  1071  eximal  1788  nfnbi  1860  19.43  1888  19.37v  1998  19.37  2228  sbrimOLD  2305  sbor  2307  dfsb3  2499  mo4f  2568  2mos  2652  neor  3037  r3al  3127  r19.23v  3209  r19.23t  3243  r19.43  3279  ceqsralt  3461  ralab  3629  ralabOLD  3630  ralrab  3631  euind  3662  reu2  3663  rmo4  3668  rmo3f  3672  rmo4f  3673  reuind  3691  2reu5lem3  3695  rmo3  3826  dfdif3  4053  raldifb  4083  elunant  4116  inssdif0  4308  ssundif  4423  dfif2  4466  pwss  4563  ralsnsg  4609  ralsng  4614  disjsn  4652  snssg  4723  raldifsni  4733  raldifsnb  4734  unissb  4878  intprg  4917  intprOLD  4919  dfiin2g  4966  disjor  5058  dftr2  5197  axrep1  5214  axrep6  5220  axpweq  5290  zfpow  5292  axpow2  5293  reusv2lem4  5327  reusv2  5329  dffr6  5546  raliunxp  5745  idrefALT  6015  asymref2  6019  dffun2  6440  dffun4  6442  dffun5  6443  dffun7  6457  fununi  6505  fvn0ssdmfun  6946  dff13  7122  dff14b  7138  zfun  7580  uniex2  7582  dfom2  7702  fimaxg  9022  fiint  9052  dfsup2  9164  fiming  9218  oemapso  9401  scottexs  9629  scott0s  9630  iscard2  9718  acnnum  9792  dfac9  9876  dfacacn  9881  kmlem4  9893  kmlem12  9901  axpowndlem3  10339  zfcndun  10355  zfcndpow  10356  zfcndac  10359  axgroth5  10564  axgroth6  10568  addsrmo  10813  mulsrmo  10814  infm3  11917  raluz2  12619  nnwos  12637  ralrp  12732  cotr2g  14668  lo1resb  15254  rlimresb  15255  o1resb  15256  modfsummod  15487  isprm4  16370  acsfn1  17351  acsfn2  17353  lublecllem  18059  isirred2  19924  isdomn2  20551  iunocv  20867  ist1-2  22479  isnrm2  22490  dfconn2  22551  alexsubALTlem3  23181  ismbl  24671  dyadmbllem  24744  ellimc3  25024  dchrelbas2  26366  dchrelbas3  26367  isch2  29564  choc0  29667  h1dei  29891  mdsl2i  30663  disjorf  30897  bnj1101  32743  bnj1109  32745  bnj1533  32811  bnj580  32872  bnj864  32881  bnj865  32882  bnj978  32908  bnj1049  32933  bnj1090  32938  bnj1145  32952  fineqvpow  33044  axextprim  33621  axunprim  33623  axpowprim  33624  untuni  33629  3orit  33637  biimpexp  33638  fnssintima  33655  ralxp3f  33664  elintfv  33717  dfon2lem8  33745  frpoins3xpg  33766  frpoins3xp3g  33767  xpord2ind  33773  xpord3ind  33779  soseq  33782  eqscut2  33979  dfom5b  34193  rdgeqoa  35520  wl-equsalcom  35680  poimirlem25  35781  poimirlem30  35786  tsim1  36267  inxpss  36426  idinxpss  36427  idinxpssinxp  36431  ineleq  36465  cocossss  36538  cosscnvssid3  36573  trcoss2  36581  redundpbi1  36723  dfeldisj3  36809  cvlsupr3  37337  pmapglbx  37762  isltrn2N  38113  cdlemefrs29bpre0  38389  3factsumint2  40010  3factsumint3  40011  3factsumint4  40012  3factsumint  40013  aks4d1p7  40071  aks4d1p8  40075  isdomn5  40151  fphpd  40618  dford4  40831  fnwe2lem2  40856  isdomn3  41009  ifpidg  41060  ifpid1g  41063  ifpor123g  41077  dfsucon  41092  undmrnresiss  41165  elintima  41214  df3or2  41329  dfhe3  41336  dffrege76  41500  dffrege115  41539  frege131  41555  ntrneikb  41657  ismnuprim  41865  ismnushort  41872  pm14.12  41992  dfvd2an  42155  dfvd3  42164  dfvd3an  42167  uun2221  42386  uun2221p1  42387  uun2221p2  42388  disjinfi  42684  supxrleubrnmptf  42945  fsummulc1f  43066  fsumiunss  43070  fnlimfvre2  43172  limsupreuz  43232  limsupvaluz2  43233  dvmptmulf  43432  dvnmul  43438  dvmptfprodlem  43439  dvnprodlem2  43442  sge0ltfirpmpt2  43918  hoidmv1le  44086  hoidmvle  44092  vonioolem2  44173  smflimlem3  44259  2reu8i  44556  ichexmpl2  44874  setrec2  46353  aacllem  46457