Theorem imbi1i 352

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 350	. 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  469  imor  866  3jaob  1453  eximal  1812  nfnbi  1885  19.43  1912  19.37v  2027  19.37  2268  sbor  2341  sb8v  2385  sb8f  2386  dfsb3  2526  mo4f  2595  2mos  2677  neor  3050  r19.43  3133  r19.23v  3192  r3al  3203  r19.23t  3261  sbralieOLD  3344  ceqsralt  3489  ralab  3656  ralrab  3657  euind  3687  reu2  3688  rmo4  3693  rmo3f  3697  rmo4f  3698  reuind  3716  2reu5lem3  3720  rmo3  3842  dfdif3OLD  4073  raldifb  4103  elunant  4137  ralin  4202  inssdif0OLD  4330  ssundif  4448  dfif2  4489  pwss  4586  ralsnsg  4636  ralsng  4641  disjsn  4677  snssb  4748  raldifsni  4763  raldifsnb  4764  unissb  4906  intprg  4946  dfiin2g  4995  iunssf  5007  iunss  5009  disjor  5091  dftr2  5220  axrep1  5239  axrep4v  5243  axrep4  5244  axrep6OLD  5248  axpweq  5321  zfpow  5337  axpow2  5338  reusv2lem4  5372  reusv2  5374  elOLD  5420  dffr6  5617  raliunxp  5825  cotrg  6111  idrefALT  6113  cnvsym  6114  asymref2  6117  dffun4  6549  dffun5  6550  dffun7  6563  fununi  6611  fvn0ssdmfun  7069  dff13  7252  dff14b  7269  fnssintima  7360  zfun  7733  uniex2OLD  7736  dfom2  7860  ralxp3f  8129  frpoins3xpg  8132  frpoins3xp3g  8133  xpord2indlem  8139  xpord3inddlem  8146  soseq  8151  fimaxg  9243  fiint  9282  dfsup2  9400  fiming  9456  oemapso  9647  scottexs  9857  scott0s  9858  iscard2  9958  acnnum  10032  dfac9  10116  dfacacn  10121  kmlem4  10133  kmlem12  10141  axpowndlem3  10579  zfcndun  10595  zfcndpow  10596  zfcndac  10599  axgroth5  10804  axgroth6  10808  addsrmo  11053  mulsrmo  11054  infm3  12169  raluz2  12916  nnwos  12934  ralrp  13033  cotr2g  15009  lo1resb  15611  rlimresb  15612  o1resb  15613  modfsummod  15842  isprm4  16737  acsfn1  17712  acsfn2  17714  lublecllem  18409  isirred2  20499  isdomn5  20809  isdomn3  20813  isdomn4r  20817  iunocv  21831  ist1-2  23504  isnrm2  23515  dfconn2  23576  alexsubALTlem3  24206  ismbl  25685  dyadmbllem  25758  ellimc3  26038  dchrelbas2  27401  dchrelbas3  27402  eqcuts2  27979  addsproplem4  28165  addsproplem6  28167  addsprop  28169  negsproplem4  28224  negsproplem6  28226  negsprop  28228  mulsprop  28323  onsis  28467  ons2ind  28468  isch2  31575  choc0  31678  h1dei  31902  mdsl2i  32674  disjorf  32924  bnj1101  35173  bnj1109  35175  bnj1533  35240  bnj580  35301  bnj864  35310  bnj865  35311  bnj978  35337  bnj1049  35362  bnj1090  35367  bnj1145  35381  fineqvpow  35528  axpowg  35559  vonf1wev  35592  vonf1owevOLD  35594  antnestALT  36186  axextprim  36193  axunprim  36195  axpowprim  36196  untuni  36201  3orit  36208  biimpexp  36209  elintfv  36257  dfon2lem8  36280  dfom5b  36402  iineq1i  36708  ixpeq1i  36712  ss-ax8  36737  mh-regprimbi  37056  mh-infprim2bi  37058  rdgeqoa  38016  wl-equsalcom  38198  wl-sb9v  38204  poimirlem25  38296  poimirlem30  38301  tsim1  38779  inxpss  38966  idinxpss  38967  ref5  38968  idinxpssinxp  38972  ineleq  39003  cocossss  39175  cosscnvssid3  39215  trcoss2  39223  redundpbi1  39364  dfeldisj3  39460  qmapeldisjsim  39509  dfantisymrel5  39514  antisymrelres  39515  cvlsupr3  40118  pmapglbx  40543  isltrn2N  40894  cdlemefrs29bpre0  41170  3factsumint2  42789  3factsumint3  42790  3factsumint4  42791  3factsumint  42792  aks4d1p7  42850  aks4d1p8  42854  fphpd  43543  dford4  43756  fnwe2lem2  43778  unielss  43945  safesnsupfilb  44144  faosnf0.11b  44153  ifpidg  44217  ifpid1g  44220  ifpor123g  44234  dfsucon  44249  undmrnresiss  44330  elintima  44379  df3or2  44494  dfhe3  44501  dffrege76  44665  dffrege115  44704  frege131  44720  ntrneikb  44820  ismnuprim  45004  ismnushort  45011  pm14.12  45131  dfvd2an  45291  dfvd3  45300  dfvd3an  45303  uun2221  45521  uun2221p1  45522  uun2221p2  45523  sswfaxreg  45696  modelac8prim  45701  disjinfi  45910  supxrleubrnmptf  46165  fsummulc1f  46287  fsumiunss  46291  fnlimfvre2  46391  limsupreuz  46451  dvmptmulf  46651  dvnmul  46657  dvmptfprodlem  46658  dvnprodlem2  46661  sge0ltfirpmpt2  47140  hoidmv1le  47308  hoidmvle  47314  vonioolem2  47395  smflimlem3  47487  2reu8i  47850  ichexmpl2  48219  setrec2  50473  aacllem  50621