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 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  466  imor  851  ifpnOLD  1073  eximal  1782  nfnbi  1855  19.43  1883  19.37v  1993  19.37  2223  sbrimOLD  2300  sbor  2302  sb8v  2348  sb8f  2349  dfsb3  2496  mo4f  2565  2mos  2649  neor  3034  r19.43  3122  r19.23v  3176  r3al  3190  r19.23t  3235  ceqsralt  3468  ralab  3633  ralabOLD  3634  ralrab  3635  euind  3664  reu2  3665  rmo4  3670  rmo3f  3674  rmo4f  3675  reuind  3693  2reu5lem3  3697  rmo3  3827  dfdif3  4055  raldifb  4085  elunant  4118  inssdif0  4309  ssundif  4424  dfif2  4467  pwss  4562  ralsnsg  4608  ralsng  4613  disjsn  4651  snssb  4722  snssgOLD  4724  raldifsni  4734  raldifsnb  4735  unissb  4879  unissbOLD  4880  intprg  4919  intprOLD  4921  dfiin2g  4969  disjor  5061  dftr2  5200  axrep1  5219  axrep6  5225  axpweq  5296  zfpow  5298  axpow2  5299  reusv2lem4  5333  reusv2  5335  el  5370  dffr6  5558  raliunxp  5761  cotrg  6027  cotrgOLD  6028  idrefALT  6031  cnvsym  6032  cnvsymOLD  6033  asymref2  6037  dffun2OLDOLD  6470  dffun4  6474  dffun5  6475  dffun7  6490  fununi  6538  fvn0ssdmfun  6984  dff13  7160  dff14b  7176  zfun  7621  uniex2  7623  dfom2  7746  fimaxg  9105  fiint  9135  dfsup2  9247  fiming  9301  oemapso  9484  scottexs  9689  scott0s  9690  iscard2  9778  acnnum  9854  dfac9  9938  dfacacn  9943  kmlem4  9955  kmlem12  9963  axpowndlem3  10401  zfcndun  10417  zfcndpow  10418  zfcndac  10421  axgroth5  10626  axgroth6  10630  addsrmo  10875  mulsrmo  10876  infm3  11980  raluz2  12683  nnwos  12701  ralrp  12796  cotr2g  14732  lo1resb  15318  rlimresb  15319  o1resb  15320  modfsummod  15551  isprm4  16434  acsfn1  17415  acsfn2  17417  lublecllem  18123  isirred2  19988  isdomn2  20615  iunocv  20931  ist1-2  22543  isnrm2  22554  dfconn2  22615  alexsubALTlem3  23245  ismbl  24735  dyadmbllem  24808  ellimc3  25088  dchrelbas2  26430  dchrelbas3  26431  isch2  29630  choc0  29733  h1dei  29957  mdsl2i  30729  disjorf  30963  bnj1101  32809  bnj1109  32811  bnj1533  32877  bnj580  32938  bnj864  32947  bnj865  32948  bnj978  32974  bnj1049  32999  bnj1090  33004  bnj1145  33018  fineqvpow  33110  axextprim  33687  axunprim  33689  axpowprim  33690  untuni  33695  3orit  33703  biimpexp  33704  fnssintima  33721  ralxp3f  33730  elintfv  33783  dfon2lem8  33811  frpoins3xpg  33832  frpoins3xp3g  33833  xpord2ind  33839  xpord3ind  33845  soseq  33848  eqscut2  34045  dfom5b  34259  rdgeqoa  35585  wl-equsalcom  35745  poimirlem25  35846  poimirlem30  35851  tsim1  36332  inxpss  36489  idinxpss  36490  idinxpssinxp  36494  ineleq  36528  cocossss  36601  cosscnvssid3  36636  trcoss2  36644  redundpbi1  36786  dfeldisj3  36872  cvlsupr3  37400  pmapglbx  37825  isltrn2N  38176  cdlemefrs29bpre0  38452  3factsumint2  40072  3factsumint3  40073  3factsumint4  40074  3factsumint  40075  aks4d1p7  40133  aks4d1p8  40137  isdomn5  40213  fphpd  40675  dford4  40889  fnwe2lem2  40914  isdomn3  41067  ifpidg  41136  ifpid1g  41139  ifpor123g  41153  dfsucon  41168  undmrnresiss  41250  elintima  41299  df3or2  41414  dfhe3  41421  dffrege76  41585  dffrege115  41624  frege131  41640  ntrneikb  41742  ismnuprim  41950  ismnushort  41957  pm14.12  42077  dfvd2an  42240  dfvd3  42249  dfvd3an  42252  uun2221  42471  uun2221p1  42472  uun2221p2  42473  disjinfi  42775  supxrleubrnmptf  43039  fsummulc1f  43161  fsumiunss  43165  fnlimfvre2  43267  limsupreuz  43327  limsupvaluz2  43328  dvmptmulf  43527  dvnmul  43533  dvmptfprodlem  43534  dvnprodlem2  43537  sge0ltfirpmpt2  44014  hoidmv1le  44182  hoidmvle  44188  vonioolem2  44269  smflimlem3  44361  2reu8i  44663  ichexmpl2  44980  setrec2  46459  aacllem  46563