Theorem imbi1i 353

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  ancomst  468  imor  850  ifpnOLD  1070  eximal  1784  19.43  1883  19.37v  1998  19.37  2232  sbrim  2309  sbor  2312  dfsb3  2512  dfsb3ALT  2568  sbrimALT  2585  mo4f  2626  2mos  2711  neor  3078  r3al  3167  r19.23v  3238  r19.23t  3272  r19.43  3304  ceqsralt  3475  ralab  3632  ralrab  3633  euind  3663  reu2  3664  rmo4  3669  rmo3f  3673  rmo4f  3674  reuind  3692  2reu5lem3  3696  rmo3  3818  dfdif3  4042  raldifb  4072  elunant  4105  inssdif0  4283  ssundif  4391  dfif2  4427  pwss  4522  ralsnsg  4568  disjsn  4607  snssg  4678  raldifsni  4688  raldifsnb  4689  unissb  4832  intpr  4871  dfiin2g  4919  disjor  5010  dftr2  5138  axrep1  5155  axrep6  5161  axpweq  5230  zfpow  5232  axpow2  5233  reusv2lem4  5267  reusv2  5269  raliunxp  5674  idrefALT  5940  asymref2  5944  dffun2  6334  dffun4  6336  dffun5  6337  dffun7  6351  fununi  6399  fvn0ssdmfun  6819  dff13  6991  dff14b  7007  zfun  7442  uniex2  7444  dfom2  7562  fimaxg  8749  fiint  8779  dfsup2  8892  fiming  8946  oemapso  9129  scottexs  9300  scott0s  9301  iscard2  9389  acnnum  9463  dfac9  9547  dfacacn  9552  kmlem4  9564  kmlem12  9572  axpowndlem3  10010  zfcndun  10026  zfcndpow  10027  zfcndac  10030  axgroth5  10235  axgroth6  10239  addsrmo  10484  mulsrmo  10485  infm3  11587  raluz2  12285  nnwos  12303  ralrp  12397  cotr2g  14327  lo1resb  14913  rlimresb  14914  o1resb  14915  modfsummod  15141  isprm4  16018  acsfn1  16924  acsfn2  16926  lublecllem  17590  isirred2  19447  isdomn2  20065  iunocv  20370  ist1-2  21952  isnrm2  21963  dfconn2  22024  alexsubALTlem3  22654  ismbl  24130  dyadmbllem  24203  ellimc3  24482  dchrelbas2  25821  dchrelbas3  25822  isch2  29006  choc0  29109  h1dei  29333  mdsl2i  30105  disjorf  30342  bnj1101  32166  bnj1109  32168  bnj1533  32234  bnj580  32295  bnj864  32304  bnj865  32305  bnj978  32331  bnj1049  32356  bnj1090  32361  bnj1145  32375  axextprim  33040  axunprim  33042  axpowprim  33043  untuni  33048  3orit  33058  biimpexp  33059  elintfv  33120  dfon2lem8  33148  soseq  33209  dfom5b  33486  rdgeqoa  34787  wl-equsalcom  34947  wl-dfralflem  35003  poimirlem25  35082  poimirlem30  35087  tsim1  35568  inxpss  35729  idinxpss  35730  idinxpssinxp  35734  ineleq  35768  cocossss  35841  cosscnvssid3  35876  trcoss2  35884  redundpbi1  36026  dfeldisj3  36112  cvlsupr3  36640  pmapglbx  37065  isltrn2N  37416  cdlemefrs29bpre0  37692  3factsumint2  39310  3factsumint3  39311  3factsumint4  39312  3factsumint  39313  fphpd  39757  dford4  39970  fnwe2lem2  39995  isdomn3  40148  ifpidg  40199  ifpid1g  40202  ifpor123g  40216  dfsucon  40231  undmrnresiss  40304  elintima  40354  df3or2  40469  dfhe3  40476  dffrege76  40640  dffrege115  40679  frege131  40695  ntrneikb  40797  ismnuprim  41002  pm14.12  41125  dfvd2an  41288  dfvd3  41297  dfvd3an  41300  uun2221  41519  uun2221p1  41520  uun2221p2  41521  disjinfi  41820  supxrleubrnmptf  42090  fsummulc1f  42212  fsumiunss  42217  fnlimfvre2  42319  limsupreuz  42379  limsupvaluz2  42380  dvmptmulf  42579  dvnmul  42585  dvmptfprodlem  42586  dvnprodlem2  42589  sge0ltfirpmpt2  43065  hoidmv1le  43233  hoidmvle  43239  vonioolem2  43320  smflimlem3  43406  2reu8i  43669  ichexmpl2  43987  setrec2  45225  aacllem  45329