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 ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  ancomst  470  imor  867  3jaob  1453  eximal  1815  nfnbi  1888  19.43  1915  19.37v  2030  19.37  2269  sbor  2340  sb8v  2383  sb8f  2384  dfsb3  2524  mo4f  2593  2mos  2675  neor  3048  r19.43  3131  r19.23v  3190  r3al  3201  r19.23t  3259  sbralieOLD  3341  ceqsralt  3485  ralab  3651  ralrab  3652  euind  3682  reu2  3683  rmo4  3688  rmo3f  3692  rmo4f  3693  reuind  3711  2reu5lem3  3715  rmo3  3836  raldifb  4096  elunant  4130  ralin  4195  inssdif0OLD  4323  ssundif  4443  dfif2  4484  pwss  4581  ralsnsg  4631  ralsng  4636  disjsn  4672  snssb  4743  raldifsni  4758  raldifsnb  4759  unissb  4901  intprg  4941  dfiin2g  4989  iunssf  5001  iunss  5003  disjor  5085  dftr2  5214  axrep1  5233  axrep4v  5237  axrep4  5238  axpweq  5312  zfpow  5328  axpow2  5329  reusv2lem4  5363  reusv2  5365  el.OLD  5407  dffr6  5607  raliunxp  5816  cotrg  6105  idrefALT  6107  cnvsym  6108  asymref2  6111  dffun4  6550  dffun5  6551  dffun7  6565  fununi  6613  fvn0ssdmfun  7072  dff13  7256  dff14b  7273  fnssintima  7370  zfun  7750  uniex2OLD  7753  dfom2  7877  ralxp3f  8147  frpoins3xpg  8150  frpoins3xp3g  8151  xpord2indlem  8157  xpord3inddlem  8164  soseq  8169  fimaxg  9271  fiint  9311  dfsup2  9429  fiming  9485  oemapso  9676  scottexsOLD  9936  scott0bsOLD  9938  setrec2  9970  iscard2  10050  acnnum  10124  dfac9  10208  dfacacn  10213  kmlem4  10225  kmlem12  10233  axpowndlem3  10677  zfcndun  10693  zfcndpow  10694  zfcndac  10697  axgroth5  10902  axgroth6  10906  addsrmo  11151  mulsrmo  11152  infm3  12269  raluz2  13017  nnwos  13035  ralrp  13135  cotr2g  15122  lo1resb  15724  rlimresb  15725  o1resb  15726  modfsummod  15954  isprm4  16852  acsfn1  17828  acsfn2  17830  lublecllem  18525  isirred2  20644  isdomn5  20955  isdomn3  20959  isdomn4r  20963  iunocv  21980  ist1-2  23658  isnrm2  23669  dfconn2  23730  alexsubALTlem3  24361  ismbl  25840  dyadmbllem  25913  ellimc3  26192  dchrelbas2  27557  dchrelbas3  27558  eqcuts2  28165  addsproplem4  28351  addsproplem6  28353  addsprop  28355  negsproplem4  28410  negsproplem6  28412  negsprop  28414  mulsprop  28509  onsis  28653  ons2ind  28654  isch2  31818  choc0  31921  h1dei  32145  mdsl2i  32917  disjorf  33166  bnj1101  35408  bnj1109  35410  bnj1533  35475  bnj580  35536  bnj864  35545  bnj865  35546  bnj978  35572  bnj1049  35597  bnj1090  35602  bnj1145  35616  fineqvpow  35766  axpowg  35797  vonf1wev  35870  vonf1owevOLD  35872  antnestALT  36438  axextprim  36445  axunprim  36447  axpowprim  36448  untuni  36453  3orit  36460  biimpexp  36461  elintfv  36509  dfon2lem8  36532  dfom5b  36654  iineq1i  36965  ixpeq1i  36969  ss-ax8  36994  mh-regprimbi  37313  mh-infprim2bi  37315  rdgeqoa  38273  wl-equsalcom  38455  wl-sb9v  38461  poimirlem25  38543  poimirlem30  38548  tsim1  39042  inxpss  39229  idinxpss  39230  ref5  39231  idinxpssinxp  39235  ineleq  39266  cocossss  39438  cosscnvssid3  39478  trcoss2  39486  redundpbi1  39627  dfeldisj3  39723  qmapeldisjsim  39772  dfantisymrel5  39777  antisymrelres  39778  cvlsupr3  40381  pmapglbx  40806  isltrn2N  41157  cdlemefrs29bpre0  41433  3factsumint2  43052  3factsumint3  43053  3factsumint4  43054  3factsumint  43055  aks4d1p7  43113  aks4d1p8  43117  fphpd  43802  dford4  44015  fnwe2lem2  44037  unielss  44204  safesnsupfilb  44403  faosnf0.11b  44412  ifpidg  44476  ifpid1g  44479  ifpor123g  44493  dfsucon  44508  undmrnresiss  44589  elintima  44638  df3or2  44753  dfhe3  44760  dffrege76  44924  dffrege115  44963  frege131  44979  ntrneikb  45079  ismnuprim  45263  ismnushort  45270  pm14.12  45390  dfvd2an  45550  dfvd3  45559  dfvd3an  45562  uun2221  45780  uun2221p1  45781  uun2221p2  45782  sswfaxreg  45955  modelac8prim  45960  disjinfi  46176  supxrleubrnmptf  46430  fsummulc1f  46552  fsumiunss  46556  fnlimfvre2  46656  limsupreuz  46716  dvmptmulf  46916  dvnmul  46922  dvmptfprodlem  46923  dvnprodlem2  46926  sge0ltfirpmpt2  47405  hoidmv1le  47573  hoidmvle  47579  vonioolem2  47660  smflimlem3  47752  2reu8i  48152  ichexmpl2  48521  aacllem  50908