Theorem imbi2i 337

Description: Introduce an antecedent to both sides of a logical equivalence. This and the next three rules are useful for building up wff's around a definition, in order to make use of the definition. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)

Hypothesis

Ref	Expression
imbi2i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
imbi2i	⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))

Proof of Theorem imbi2i

Step	Hyp	Ref	Expression
1		imbi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝜒 → (𝜑 ↔ 𝜓))
3	2	pm5.74i 272	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:  jcn  338  iman  402  anidmdbi  566  pm5.32  574  pm4.14  803  nan  826  imimorb  943  pm5.6  994  nannan  1480  alimex  1810  19.36v  1969  sbal  2129  19.36  2195  2sb6  2244  sbn  2251  sbanOLD  2276  sblim  2278  sbanvOLD  2289  sbhb  2515  sbanALT  2562  dfmo  2639  moeuOLD  2642  moabsOLD  2646  eu1  2657  eu1OLD  2658  ralbii  3130  r19.21v  3140  r2allem  3165  r3al  3167  r19.21t  3179  rspc2gv  3566  reu2  3645  reu8  3653  2reu5lem3  3677  rmoanim  3801  rmoanimALT  3802  dfdif3  4007  ssconb  4030  ssin  4122  difin  4153  reldisj  4310  ssundif  4341  reuprg0  4539  raldifsni  4629  pwpw0  4647  pwsnALT  4732  unissb  4770  moabex  5236  dffr2  5400  dfepfr  5420  ssrel2  5537  dffr3  5830  opreu2reurex  6012  dffr4  6031  fncnv  6289  fun11  6290  dff13  6869  marypha2lem3  8737  dfsup2  8744  wemapsolem  8850  inf2  8921  axinf2  8938  aceq1  9378  aceq0  9379  kmlem14  9424  dfackm  9427  zfac  9717  ac6n  9742  zfcndrep  9871  zfcndac  9876  axgroth6  10085  axgroth4  10089  grothprim  10091  prime  11901  raluz2  12135  fsuppmapnn0ub  13201  mptnn0fsuppr  13205  brtrclfv  14184  rpnnen2lem12  15399  isprm2  15843  isprm4  15845  pgpfac1  18907  pgpfac  18911  isirred2  19129  pmatcollpw2lem  21057  isclo2  21368  lmres  21580  ist1-2  21627  is1stc2  21722  alexsubALTlem3  22329  itg2cn  24035  ellimc3  24148  plydivex  24557  vieta1  24572  dchrelbas2  25483  nmobndseqi  28235  nmobndseqiALT  28236  cvnbtwn3  29744  elat2  29796  ssrelf  30031  isarchi2  30410  archiabl  30423  islinds5  30535  esumcvgre  30923  signstfvneq0  31415  hashreprin  31464  breprexp  31477  bnj1098  31628  bnj1533  31696  bnj121  31714  bnj124  31715  bnj130  31718  bnj153  31724  bnj207  31725  bnj611  31762  bnj864  31766  bnj865  31767  bnj1000  31785  bnj978  31793  bnj1021  31808  bnj1047  31815  bnj1049  31816  bnj1090  31821  bnj1110  31824  bnj1128  31832  bnj1145  31835  bnj1171  31842  bnj1172  31843  bnj1174  31845  bnj1176  31847  bnj1280  31862  axinfprim  32485  dfon2lem9  32589  conway  32818  dffun10  32929  elicc3  33219  filnetlem4  33283  df3nandALT1  33301  df3nandALT2  33302  bj-ssbeq  33529  bj-ax12ssb  33534  bj-sbnf  33678  pibt2  34175  wl-dfralsb  34314  wl-dfrexex  34327  wl-dfrexsb  34328  wl-dfrmosb  34330  poimirlem30  34399  inxpssidinxp  35053  lcvnbtwn3  35645  isat3  35924  cdleme25cv  36975  cdlemefrs29bpre0  37013  cdlemk35  37529  sn-axrep5v  38588  dford4  39062  ifpidg  39293  ifpid1g  39296  ifpim23g  39297  ifpororb  39307  ifpbibib  39312  elinintrab  39373  undmrnresiss  39400  cotrintab  39410  elintima  39434  frege60b  39687  frege91  39736  frege97  39742  frege98  39743  dffrege99  39744  frege109  39754  frege110  39755  frege131  39776  frege133  39778  ntrneiiso  39877  int-sqdefd  39972  int-sqgeq0d  39977  ismnuprim  40079  pm10.541  40189  pm13.196a  40236  2sbc6g  40237  expcomdg  40325  impexpd  40338  supxrleubrnmptf  41223  fsummulc1f  41347  fsumiunss  41352  fnlimfvre2  41454  limsupreuz  41514  limsupvaluz2  41515  lmbr3v  41522  dvmptmulf  41717  dvmptfprodlem  41724  sge0ltfirpmpt2  42204  hoidmv1le  42372  hoidmvle  42378  vonioolem2  42459  smflimlem3  42545  ldepslinc  43998  setrec1lem2  44225  setrec2  44232  sbidd-misc  44252