MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi2i Structured version   Visualization version   GIF version

Theorem imbi2i 326
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
StepHypRef Expression
1 imbi2i.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝜒 → (𝜑𝜓))
32pm5.74i 260 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  iman  440  pm4.14  601  nan  603  pm5.32  667  anidmdbi  677  imimorb  920  pm5.6  950  nannan  1448  alimex  1755  19.36v  1901  19.36  2096  sblim  2396  sban  2398  sbhb  2437  2sb6  2443  mo2v  2476  moabs  2500  eu1  2509  r2allem  2933  r3al  2936  r19.21t  2951  r19.21v  2956  ralbii  2976  r19.35  3078  rspc2gv  3310  reu2  3381  reu8  3389  2reu5lem3  3402  ssconb  3727  ssin  3819  difin  3845  reldisj  3998  ssundif  4030  raldifsni  4300  pwpw0  4319  pwsnALT  4404  unissb  4442  moabex  4898  dffr2  5049  dfepfr  5069  ssrelOLD  5179  ssrel2  5181  dffr3  5467  dffr4  5665  fncnv  5930  fun11  5931  dff13  6477  marypha2lem3  8303  dfsup2  8310  wemapsolem  8415  inf2  8480  axinf2  8497  aceq1  8900  aceq0  8901  kmlem14  8945  dfackm  8948  zfac  9242  ac6n  9267  zfcndrep  9396  zfcndac  9401  axgroth6  9610  axgroth4  9614  grothprim  9616  prime  11418  raluz2  11697  fsuppmapnn0ub  12751  mptnn0fsuppr  12755  brtrclfv  13693  rpnnen2lem12  14898  isprm2  15338  isprm4  15340  pgpfac1  18419  pgpfac  18423  isirred2  18641  pmatcollpw2lem  20522  isclo2  20832  lmres  21044  ist1-2  21091  is1stc2  21185  alexsubALTlem3  21793  itg2cn  23470  ellimc3  23583  plydivex  23990  vieta1  24005  dchrelbas2  24896  nmobndseqi  27522  nmobndseqiALT  27523  cvnbtwn3  29035  elat2  29087  ssrelf  29309  funcnvmptOLD  29351  isarchi2  29566  archiabl  29579  esumcvgre  29976  signstfvneq0  30471  bnj1098  30615  bnj1533  30683  bnj121  30701  bnj124  30702  bnj130  30705  bnj153  30711  bnj207  30712  bnj611  30749  bnj864  30753  bnj865  30754  bnj1000  30772  bnj978  30780  bnj1021  30795  bnj1047  30802  bnj1049  30803  bnj1090  30808  bnj1110  30811  bnj1128  30819  bnj1145  30822  bnj1171  30829  bnj1172  30830  bnj1174  30832  bnj1176  30834  bnj1280  30849  axinfprim  31344  dfon2lem9  31450  dffun10  31716  elicc3  32006  filnetlem4  32071  df3nandALT1  32091  df3nandALT2  32092  bj-ssbeq  32322  bj-ssb0  32323  bj-ax12ssb  32330  bj-ssbn  32336  bj-sbnf  32524  wl-nannan  32969  poimirlem30  33110  lcvnbtwn3  33834  isat3  34113  cdleme25cv  35165  cdlemefrs29bpre0  35203  cdlemk35  35719  dford4  37115  ifpidg  37356  ifpid1g  37359  ifpim23g  37360  ifpororb  37370  ifpbibib  37375  elinintrab  37403  undmrnresiss  37430  cotrintab  37441  elintima  37465  frege60b  37720  frege91  37769  frege97  37775  frege98  37776  dffrege99  37777  frege109  37787  frege110  37788  frege131  37809  frege133  37811  ntrneiiso  37910  int-sqdefd  38005  int-sqgeq0d  38010  pm10.541  38087  pm13.196a  38136  2sbc6g  38137  expcomdg  38227  impexpd  38240  jcn  38727  fsummulc1f  39238  fsumiunss  39243  fnlimfvre2  39345  limsupreuz  39405  limsupvaluz2  39406  dvmptmulf  39489  dvmptfprodlem  39496  sge0ltfirpmpt2  39980  hoidmv1le  40145  hoidmvle  40151  vonioolem2  40232  smflimlem3  40318  rmoanim  40513  ldepslinc  41616  setrec1lem2  41758  setrec2  41765  sbidd-misc  41783
  Copyright terms: Public domain W3C validator