Theorem imbi2i 335

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 270	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:  jcndOLD  336  iman  402  anidmdbi  566  pm5.32  574  pm4.14  805  nan  828  imimorb  949  pm5.6  1000  nannan  1495  alimex  1833  19.36v  1991  2sb6  2089  sbrimvw  2094  sbal  2159  19.36  2223  sbn  2276  sbrim  2300  sblim  2302  cbvsbvf  2360  sbhb  2520  dfmo  2590  eu1  2606  r2allem  3142  r19.21vOLD  3180  r3al  3196  r19.21t  3250  nfra2wOLD  3297  rspc2gv  3621  reu2  3721  reu8  3729  2reu5lem3  3753  rmoanim  3888  rmoanimALT  3889  dfdif3  4114  ssconb  4137  ssin  4230  difin  4261  reldisj  4451  reldisjOLD  4452  ssundif  4487  ralidmw  4507  ralidm  4511  reuprg0  4706  raldifsni  4798  pwpw0  4816  pwsnOLD  4901  unissb  4943  unissbOLD  4944  moabex  5459  dffr2  5640  dffr2ALT  5641  dfepfr  5661  ssrel2  5785  dffr3  6098  opreu2reurex  6293  dffr4  6320  fncnv  6621  fun11  6622  dff13  7256  naddssim  8686  marypha2lem3  9434  dfsup2  9441  wemapsolem  9547  inf2  9620  axinf2  9637  aceq1  10114  aceq0  10115  kmlem14  10160  dfackm  10163  zfac  10457  ac6n  10482  zfcndrep  10611  zfcndac  10616  axgroth6  10825  axgroth4  10829  grothprim  10831  prime  12647  raluz2  12885  fsuppmapnn0ub  13964  mptnn0fsuppr  13968  brtrclfv  14953  rpnnen2lem12  16172  isprm2  16623  isprm4  16625  pgpfac1  19991  pgpfac  19995  isirred2  20312  isdomn5  21117  pmatcollpw2lem  22499  isclo2  22812  lmres  23024  ist1-2  23071  is1stc2  23166  alexsubALTlem3  23773  itg2cn  25505  ellimc3  25620  plydivex  26034  vieta1  26049  dchrelbas2  26964  conway  27525  nmobndseqi  30287  nmobndseqiALT  30288  cvnbtwn3  31796  elat2  31848  inpr0  32024  ssrelf  32099  isarchi2  32589  archiabl  32602  islinds5  32742  esumcvgre  33375  signstfvneq0  33869  hashreprin  33918  breprexp  33931  bnj1098  34080  bnj1533  34149  bnj121  34167  bnj124  34168  bnj130  34171  bnj153  34177  bnj207  34178  bnj611  34215  bnj864  34219  bnj865  34220  bnj1000  34238  bnj978  34246  bnj1021  34263  bnj1047  34270  bnj1049  34271  bnj1090  34276  bnj1110  34279  bnj1128  34287  bnj1145  34290  bnj1171  34297  bnj1172  34298  bnj1174  34300  bnj1176  34302  bnj1280  34317  axinfprim  34967  dfon2lem9  35055  dffun10  35178  elicc3  35505  filnetlem4  35569  df3nandALT1  35587  df3nandALT2  35588  bj-ssbeq  35833  bj-ax12ssb  35838  bj-sbnf  36022  pibt2  36601  poimirlem30  36821  inxpssidinxp  37488  cnvref5  37523  lcvnbtwn3  38201  isat3  38480  cdleme25cv  39532  cdlemefrs29bpre0  39570  cdlemk35  40086  dvrelogpow2b  41239  aks4d1p1p4  41242  aks6d1c2p2  41263  metakunt6  41296  metakunt24  41314  2xp3dxp2ge1d  41328  sn-axrep5v  41339  dford4  42070  ifpidg  42544  ifpid1g  42547  ifpim23g  42548  ifpororb  42558  ifpbibib  42563  elinintrab  42630  undmrnresiss  42657  cotrintab  42667  elintima  42706  frege60b  42958  frege91  43007  frege97  43013  frege98  43014  dffrege99  43015  frege109  43025  frege110  43026  frege131  43047  frege133  43049  ntrneiiso  43144  int-sqdefd  43235  int-sqgeq0d  43240  ismnuprim  43355  pm10.541  43428  pm13.196a  43475  2sbc6g  43476  expcomdg  43563  impexpd  43576  supxrleubrnmptf  44460  fsummulc1f  44586  fsumiunss  44590  fnlimfvre2  44692  limsupreuz  44752  limsupvaluz2  44753  lmbr3v  44760  dvmptmulf  44952  dvmptfprodlem  44959  sge0ltfirpmpt2  45441  hoidmv1le  45609  hoidmvle  45615  vonioolem2  45696  smflimlem3  45788  ldepslinc  47278  map0cor  47609  setrec1lem2  47821  setrec2  47828  sbidd-misc  47852