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

Theorem imbi2i 325
 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  439  pm4.14  603  nan  605  pm5.32  671  anidmdbi  681  imimorb  957  pm5.6  989  nannan  1600  alimex  1907  19.36v  2069  19.36  2245  sblim  2534  sban  2536  sbhb  2575  2sb6  2581  mo2v  2614  moabs  2639  eu1  2648  r2allem  3075  r3al  3078  r19.21t  3093  r19.21v  3098  ralbii  3118  r19.35  3222  rspc2gv  3460  reu2  3535  reu8  3543  2reu5lem3  3556  dfdif3  3863  ssconb  3886  ssin  3978  difin  4004  reldisj  4163  ssundif  4196  raldifsni  4470  pwpw0  4489  pwsnALT  4581  unissb  4621  moabex  5076  dffr2  5231  dfepfr  5251  ssrelOLD  5365  ssrel2  5367  dffr3  5656  dffr4  5857  fncnv  6123  fun11  6124  dff13  6676  marypha2lem3  8510  dfsup2  8517  wemapsolem  8622  inf2  8695  axinf2  8712  aceq1  9150  aceq0  9151  kmlem14  9197  dfackm  9200  zfac  9494  ac6n  9519  zfcndrep  9648  zfcndac  9653  axgroth6  9862  axgroth4  9866  grothprim  9868  prime  11670  raluz2  11950  fsuppmapnn0ub  13009  mptnn0fsuppr  13013  brtrclfv  13962  rpnnen2lem12  15173  isprm2  15617  isprm4  15619  pgpfac1  18699  pgpfac  18703  isirred2  18921  pmatcollpw2lem  20804  isclo2  21114  lmres  21326  ist1-2  21373  is1stc2  21467  alexsubALTlem3  22074  itg2cn  23749  ellimc3  23862  plydivex  24271  vieta1  24286  dchrelbas2  25182  nmobndseqi  27964  nmobndseqiALT  27965  cvnbtwn3  29477  elat2  29529  ssrelf  29755  funcnvmptOLD  29797  isarchi2  30069  archiabl  30082  esumcvgre  30483  signstfvneq0  30979  hashreprin  31028  breprexp  31041  bnj1098  31182  bnj1533  31250  bnj121  31268  bnj124  31269  bnj130  31272  bnj153  31278  bnj207  31279  bnj611  31316  bnj864  31320  bnj865  31321  bnj1000  31339  bnj978  31347  bnj1021  31362  bnj1047  31369  bnj1049  31370  bnj1090  31375  bnj1110  31378  bnj1128  31386  bnj1145  31389  bnj1171  31396  bnj1172  31397  bnj1174  31399  bnj1176  31401  bnj1280  31416  axinfprim  31911  dfon2lem9  32022  conway  32237  dffun10  32348  elicc3  32638  filnetlem4  32703  df3nandALT1  32723  df3nandALT2  32724  bj-ssbeq  32955  bj-ssb0  32956  bj-ax12ssb  32963  bj-ssbn  32969  bj-sbnf  33156  wl-nannan  33629  poimirlem30  33770  inxpssidinxp  34428  lcvnbtwn3  34836  isat3  35115  cdleme25cv  36166  cdlemefrs29bpre0  36204  cdlemk35  36720  dford4  38116  ifpidg  38356  ifpid1g  38359  ifpim23g  38360  ifpororb  38370  ifpbibib  38375  elinintrab  38403  undmrnresiss  38430  cotrintab  38441  elintima  38465  frege60b  38719  frege91  38768  frege97  38774  frege98  38775  dffrege99  38776  frege109  38786  frege110  38787  frege131  38808  frege133  38810  ntrneiiso  38909  int-sqdefd  39004  int-sqgeq0d  39009  pm10.541  39086  pm13.196a  39135  2sbc6g  39136  expcomdg  39226  impexpd  39239  jcn  39722  supxrleubrnmptf  40196  fsummulc1f  40323  fsumiunss  40328  fnlimfvre2  40430  limsupreuz  40490  limsupvaluz2  40491  lmbr3v  40498  dvmptmulf  40673  dvmptfprodlem  40680  sge0ltfirpmpt2  41164  hoidmv1le  41332  hoidmvle  41338  vonioolem2  41419  smflimlem3  41505  rmoanim  41703  ldepslinc  42826  setrec1lem2  42963  setrec2  42970  sbidd-misc  42991
 Copyright terms: Public domain W3C validator