Theorem imbi1i 350

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 348	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)))
3	1, 2	ax-mp 5	1 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  ancomst  465  imor  859  3jaob  1434  eximal  1789  nfnbi  1862  19.43  1889  19.37v  2004  19.37  2244  sbor  2317  sb8v  2361  sb8f  2362  dfsb3  2502  mo4f  2571  2mos  2653  neor  3026  r19.43  3107  r19.23v  3166  r3al  3177  r19.23t  3235  sbralieOLD  3319  ceqsralt  3465  ralab  3634  ralrab  3635  euind  3665  reu2  3666  rmo4  3671  rmo3f  3675  rmo4f  3676  reuind  3694  2reu5lem3  3698  rmo3  3821  dfdif3OLD  4049  raldifb  4079  elunant  4113  ralin  4177  inssdif0  4302  ssundif  4415  dfif2  4456  pwss  4552  ralsnsg  4602  ralsng  4607  disjsn  4643  snssb  4714  raldifsni  4728  raldifsnb  4729  unissb  4871  intprg  4911  dfiin2g  4960  iunssf  4972  iunss  4974  disjor  5054  dftr2  5181  axrep1  5200  axrep4v  5204  axrep4  5205  axrep6OLD  5209  axpweq  5279  zfpow  5295  axpow2  5296  reusv2lem4  5330  reusv2  5332  elOLD  5378  dffr6  5574  raliunxp  5781  cotrg  6061  idrefALT  6063  cnvsym  6064  asymref2  6067  dffun4  6498  dffun5  6499  dffun7  6512  fununi  6560  fvn0ssdmfun  7015  dff13  7198  dff14b  7215  fnssintima  7306  zfun  7679  uniex2  7681  dfom2  7808  ralxp3f  8077  frpoins3xpg  8080  frpoins3xp3g  8081  xpord2indlem  8087  xpord3inddlem  8094  soseq  8099  fimaxg  9187  fiint  9227  dfsup2  9347  fiming  9403  oemapso  9594  scottexs  9802  scott0s  9803  iscard2  9891  acnnum  9965  dfac9  10050  dfacacn  10055  kmlem4  10067  kmlem12  10075  axpowndlem3  10513  zfcndun  10529  zfcndpow  10530  zfcndac  10533  axgroth5  10738  axgroth6  10742  addsrmo  10987  mulsrmo  10988  infm3  12106  raluz2  12838  nnwos  12856  ralrp  12955  cotr2g  14929  lo1resb  15517  rlimresb  15518  o1resb  15519  modfsummod  15748  isprm4  16644  acsfn1  17618  acsfn2  17620  lublecllem  18315  isirred2  20392  isdomn5  20682  isdomn2OLD  20684  isdomn3  20687  isdomn4r  20691  iunocv  21656  ist1-2  23330  isnrm2  23341  dfconn2  23402  alexsubALTlem3  24032  ismbl  25511  dyadmbllem  25584  ellimc3  25864  dchrelbas2  27218  dchrelbas3  27219  eqcuts2  27796  addsproplem4  27982  addsproplem6  27984  addsprop  27986  negsproplem4  28041  negsproplem6  28043  negsprop  28045  mulsprop  28140  onsis  28284  ons2ind  28285  isch2  31312  choc0  31415  h1dei  31639  mdsl2i  32411  disjorf  32668  bnj1101  34967  bnj1109  34969  bnj1533  35034  bnj580  35095  bnj864  35104  bnj865  35105  bnj978  35131  bnj1049  35156  bnj1090  35161  bnj1145  35175  fineqvpow  35296  axpowg  35327  vonf1owev  35336  antnestALT  35922  axextprim  35929  axunprim  35931  axpowprim  35932  untuni  35937  3orit  35944  biimpexp  35945  elintfv  35993  dfon2lem8  36016  dfom5b  36138  iineq1i  36424  ixpeq1i  36428  ss-ax8  36453  mh-regprimbi  36773  mh-infprim2bi  36775  rdgeqoa  37732  wl-equsalcom  37914  wl-sb9v  37920  poimirlem25  38012  poimirlem30  38017  tsim1  38497  inxpss  38684  idinxpss  38685  ref5  38686  idinxpssinxp  38690  ineleq  38721  cocossss  38893  cosscnvssid3  38933  trcoss2  38941  redundpbi1  39082  dfeldisj3  39178  qmapeldisjsim  39227  dfantisymrel5  39232  antisymrelres  39233  cvlsupr3  39836  pmapglbx  40261  isltrn2N  40612  cdlemefrs29bpre0  40888  3factsumint2  42507  3factsumint3  42508  3factsumint4  42509  3factsumint  42510  aks4d1p7  42568  aks4d1p8  42572  fphpd  43261  dford4  43474  fnwe2lem2  43496  unielss  43663  safesnsupfilb  43862  faosnf0.11b  43871  ifpidg  43935  ifpid1g  43938  ifpor123g  43952  dfsucon  43967  undmrnresiss  44048  elintima  44097  df3or2  44212  dfhe3  44219  dffrege76  44383  dffrege115  44422  frege131  44438  ntrneikb  44538  ismnuprim  44738  ismnushort  44745  pm14.12  44865  dfvd2an  45026  dfvd3  45035  dfvd3an  45038  uun2221  45256  uun2221p1  45257  uun2221p2  45258  sswfaxreg  45431  modelac8prim  45436  disjinfi  45639  supxrleubrnmptf  45894  fsummulc1f  46016  fsumiunss  46020  fnlimfvre2  46120  limsupreuz  46180  dvmptmulf  46380  dvnmul  46386  dvmptfprodlem  46387  dvnprodlem2  46390  sge0ltfirpmpt2  46869  hoidmv1le  47037  hoidmvle  47043  vonioolem2  47124  smflimlem3  47216  2reu8i  47576  ichexmpl2  47945  setrec2  50185  aacllem  50291