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

Theorem imbi2i 327
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 262 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  iman  390  anidmdbi  557  pm5.32  565  pm4.14  832  nan  850  imimorb  964  pm5.6  1015  nannan  1605  alimex  1915  19.36v  2082  19.36  2265  2sb6  2288  sblim  2555  sban  2557  sbhb  2599  mo2v  2636  moabs  2661  eu1  2670  r2allem  3121  r3al  3124  r19.21t  3139  r19.21v  3144  ralbii  3164  r19.35  3268  rspc2gv  3510  reu2  3586  reu8  3594  2reu5lem3  3607  dfdif3  3913  ssconb  3936  ssin  4025  difin  4057  reldisj  4211  ssundif  4242  raldifsni  4510  pwpw0  4528  pwsnALT  4616  unissb  4656  moabex  5111  dffr2  5270  dfepfr  5290  ssrelOLD  5404  ssrel2  5406  dffr3  5702  dffr4  5903  fncnv  6167  fun11  6168  dff13  6730  marypha2lem3  8576  dfsup2  8583  wemapsolem  8688  inf2  8761  axinf2  8778  aceq1  9217  aceq0  9218  kmlem14  9264  dfackm  9267  zfac  9561  ac6n  9586  zfcndrep  9715  zfcndac  9720  axgroth6  9929  axgroth4  9933  grothprim  9935  prime  11718  raluz2  11949  fsuppmapnn0ub  13012  mptnn0fsuppr  13016  brtrclfv  13960  rpnnen2lem12  15168  isprm2  15607  isprm4  15609  pgpfac1  18675  pgpfac  18679  isirred2  18897  pmatcollpw2lem  20789  isclo2  21100  lmres  21312  ist1-2  21359  is1stc2  21453  alexsubALTlem3  22060  itg2cn  23738  ellimc3  23851  plydivex  24260  vieta1  24275  dchrelbas2  25170  nmobndseqi  27956  nmobndseqiALT  27957  cvnbtwn3  29469  elat2  29521  ssrelf  29746  funcnvmptOLD  29788  isarchi2  30058  archiabl  30071  esumcvgre  30472  signstfvneq0  30968  hashreprin  31017  breprexp  31030  bnj1098  31171  bnj1533  31239  bnj121  31257  bnj124  31258  bnj130  31261  bnj153  31267  bnj207  31268  bnj611  31305  bnj864  31309  bnj865  31310  bnj1000  31328  bnj978  31336  bnj1021  31351  bnj1047  31358  bnj1049  31359  bnj1090  31364  bnj1110  31367  bnj1128  31375  bnj1145  31378  bnj1171  31385  bnj1172  31386  bnj1174  31388  bnj1176  31390  bnj1280  31405  axinfprim  31899  dfon2lem9  32010  conway  32225  dffun10  32336  elicc3  32626  filnetlem4  32691  df3nandALT1  32709  df3nandALT2  32710  bj-ssbeq  32937  bj-ssb0  32938  bj-ax12ssb  32945  bj-ssbn  32950  bj-sbnf  33135  wl-nannan  33608  poimirlem30  33746  inxpssidinxp  34396  lcvnbtwn3  34802  isat3  35081  cdleme25cv  36133  cdlemefrs29bpre0  36171  cdlemk35  36687  dford4  38091  ifpidg  38330  ifpid1g  38333  ifpim23g  38334  ifpororb  38344  ifpbibib  38349  elinintrab  38377  undmrnresiss  38404  cotrintab  38415  elintima  38439  frege60b  38693  frege91  38742  frege97  38748  frege98  38749  dffrege99  38750  frege109  38760  frege110  38761  frege131  38782  frege133  38784  ntrneiiso  38883  int-sqdefd  38978  int-sqgeq0d  38983  pm10.541  39060  pm13.196a  39108  2sbc6g  39109  expcomdg  39198  impexpd  39211  jcn  39693  supxrleubrnmptf  40153  fsummulc1f  40276  fsumiunss  40281  fnlimfvre2  40383  limsupreuz  40443  limsupvaluz2  40444  lmbr3v  40451  dvmptmulf  40626  dvmptfprodlem  40633  sge0ltfirpmpt2  41116  hoidmv1le  41284  hoidmvle  41290  vonioolem2  41371  smflimlem3  41457  rmoanim  41685  ldepslinc  42860  setrec1lem2  42997  setrec2  43004  sbidd-misc  43025
  Copyright terms: Public domain W3C validator