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  401  anidmdbi  565  pm5.32  573  pm4.14  803  nan  826  imimorb  947  pm5.6  998  nannan  1489  alimex  1834  19.36v  1992  2sb6  2090  sbrimvlem  2095  sbal  2161  19.36  2226  sbn  2280  sblim  2306  sbievg  2361  sbhb  2525  dfmo  2596  eu1  2612  r19.21v  3100  r2allem  3123  r3al  3125  r19.21t  3137  nfra2wOLD  3152  rspc2gv  3561  reu2  3655  reu8  3663  2reu5lem3  3687  rmoanim  3823  rmoanimALT  3824  dfdif3  4045  ssconb  4068  ssin  4161  difin  4192  reldisj  4382  reldisjOLD  4383  ssundif  4415  ralidmw  4435  ralidm  4439  reuprg0  4635  raldifsni  4725  pwpw0  4743  pwsnOLD  4829  unissb  4870  moabex  5368  dffr2  5544  dffr2ALT  5545  dfepfr  5565  ssrel2  5685  dffr3  5996  opreu2reurex  6186  dffr4  6211  fncnv  6491  fun11  6492  dff13  7109  marypha2lem3  9126  dfsup2  9133  wemapsolem  9239  inf2  9311  axinf2  9328  aceq1  9804  aceq0  9805  kmlem14  9850  dfackm  9853  zfac  10147  ac6n  10172  zfcndrep  10301  zfcndac  10306  axgroth6  10515  axgroth4  10519  grothprim  10521  prime  12331  raluz2  12566  fsuppmapnn0ub  13643  mptnn0fsuppr  13647  brtrclfv  14641  rpnnen2lem12  15862  isprm2  16315  isprm4  16317  pgpfac1  19598  pgpfac  19602  isirred2  19858  pmatcollpw2lem  21834  isclo2  22147  lmres  22359  ist1-2  22406  is1stc2  22501  alexsubALTlem3  23108  itg2cn  24833  ellimc3  24948  plydivex  25362  vieta1  25377  dchrelbas2  26290  nmobndseqi  29042  nmobndseqiALT  29043  cvnbtwn3  30551  elat2  30603  inpr0  30781  ssrelf  30856  isarchi2  31341  archiabl  31354  islinds5  31465  esumcvgre  31959  signstfvneq0  32451  hashreprin  32500  breprexp  32513  bnj1098  32663  bnj1533  32732  bnj121  32750  bnj124  32751  bnj130  32754  bnj153  32760  bnj207  32761  bnj611  32798  bnj864  32802  bnj865  32803  bnj1000  32821  bnj978  32829  bnj1021  32846  bnj1047  32853  bnj1049  32854  bnj1090  32859  bnj1110  32862  bnj1128  32870  bnj1145  32873  bnj1171  32880  bnj1172  32881  bnj1174  32883  bnj1176  32885  bnj1280  32900  axinfprim  33547  dfon2lem9  33673  naddssim  33764  conway  33920  dffun10  34143  elicc3  34433  filnetlem4  34497  df3nandALT1  34515  df3nandALT2  34516  bj-ssbeq  34761  bj-ax12ssb  34766  bj-sbnf  34951  pibt2  35515  poimirlem30  35734  inxpssidinxp  36378  lcvnbtwn3  36969  isat3  37248  cdleme25cv  38299  cdlemefrs29bpre0  38337  cdlemk35  38853  dvrelogpow2b  40004  aks4d1p1p4  40007  metakunt6  40058  metakunt24  40076  2xp3dxp2ge1d  40090  isdomn5  40099  sn-axrep5v  40113  dford4  40767  ifpidg  40996  ifpid1g  40999  ifpim23g  41000  ifpororb  41010  ifpbibib  41015  elinintrab  41074  undmrnresiss  41101  cotrintab  41111  elintima  41150  frege60b  41402  frege91  41451  frege97  41457  frege98  41458  dffrege99  41459  frege109  41469  frege110  41470  frege131  41491  frege133  41493  ntrneiiso  41590  int-sqdefd  41681  int-sqgeq0d  41686  ismnuprim  41801  pm10.541  41874  pm13.196a  41921  2sbc6g  41922  expcomdg  42009  impexpd  42022  supxrleubrnmptf  42881  fsummulc1f  43002  fsumiunss  43006  fnlimfvre2  43108  limsupreuz  43168  limsupvaluz2  43169  lmbr3v  43176  dvmptmulf  43368  dvmptfprodlem  43375  sge0ltfirpmpt2  43854  hoidmv1le  44022  hoidmvle  44028  vonioolem2  44109  smflimlem3  44195  ldepslinc  45738  map0cor  46070  setrec1lem2  46280  setrec2  46287  sbidd-misc  46307