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

Theorem imbi2i 324
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 258 1 ((𝜒𝜑) ↔ (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  iman  438  pm4.14  599  nan  601  pm5.32  665  anidmdbi  675  imimorb  916  pm5.6  948  nannan  1442  alimex  1747  19.36v  1890  19.36  2084  sblim  2384  sban  2386  sbhb  2425  2sb6  2431  mo2v  2464  moabs  2488  eu1  2497  r2allem  2920  r3al  2923  r19.21t  2937  r19.21v  2942  ralbii  2962  r19.35  3064  reu2  3360  reu8  3368  2reu5lem3  3381  ssconb  3704  ssin  3796  difin  3822  reldisj  3971  ssundif  4003  raldifsni  4264  pwpw0  4283  pwsnALT  4361  unissb  4399  moabex  4847  dffr2  4992  dfepfr  5012  ssrel  5119  ssrel2  5121  dffr3  5403  dffr4  5598  fncnv  5861  fun11  5862  dff13  6393  marypha2lem3  8203  dfsup2  8210  wemapsolem  8315  inf2  8380  axinf2  8397  aceq1  8800  aceq0  8801  kmlem14  8845  dfackm  8848  zfac  9142  ac6n  9167  zfcndrep  9292  zfcndac  9297  axgroth6  9506  axgroth4  9510  grothprim  9512  prime  11292  raluz2  11571  fsuppmapnn0ub  12614  mptnn0fsuppr  12618  brtrclfv  13539  rpnnen2lem12  14741  isprm2  15181  isprm4  15183  pgpfac1  18250  pgpfac  18254  isirred2  18472  pmatcollpw2lem  20348  isclo2  20649  lmres  20861  ist1-2  20908  is1stc2  21002  alexsubALTlem3  21610  itg2cn  23280  ellimc3  23393  plydivex  23800  vieta1  23815  dchrelbas2  24706  nmobndseqi  26811  nmobndseqiALT  26812  cvnbtwn3  28324  elat2  28376  ssrelf  28598  funcnvmptOLD  28643  isarchi2  28863  archiabl  28876  esumcvgre  29273  signstfvneq0  29768  bnj1098  29901  bnj1533  29969  bnj121  29987  bnj124  29988  bnj130  29991  bnj153  29997  bnj207  29998  bnj611  30035  bnj864  30039  bnj865  30040  bnj1000  30058  bnj978  30066  bnj1021  30081  bnj1047  30088  bnj1049  30089  bnj1090  30094  bnj1110  30097  bnj1128  30105  bnj1145  30108  bnj1171  30115  bnj1172  30116  bnj1174  30118  bnj1176  30120  bnj1280  30135  axinfprim  30630  dfon2lem9  30733  dffun10  30984  elicc3  31274  filnetlem4  31339  df3nandALT1  31359  df3nandALT2  31360  bj-ssbeq  31609  bj-ssb0  31610  bj-ax12ssb  31617  bj-ssbn  31623  bj-sbnf  31809  wl-nannan  32260  poimirlem30  32392  lcvnbtwn3  33116  isat3  33395  cdleme25cv  34447  cdlemefrs29bpre0  34485  cdlemk35  35001  dford4  36397  ifpidg  36638  ifpid1g  36641  ifpim23g  36642  ifpororb  36652  ifpbibib  36657  elinintrab  36685  undmrnresiss  36712  cotrintab  36723  elintima  36747  frege60b  37002  frege91  37051  frege97  37057  frege98  37058  dffrege99  37059  frege109  37069  frege110  37070  frege131  37091  frege133  37093  ntrneiiso  37192  int-rightdistd  37288  int-sqdefd  37289  int-sqgeq0d  37294  pm10.541  37371  pm13.196a  37420  2sbc6g  37421  expcomdg  37510  impexpd  37523  jcn  38011  fsummulc1f  38418  fsumiunss  38425  fnlimfvre2  38527  dvmptmulf  38610  dvmptfprodlem  38617  sge0ltfirpmpt2  39102  hoidmv1le  39267  hoidmvle  39273  vonioolem2  39355  smflimlem3  39442  rmoanim  39611  ldepslinc  42073  sbidd-misc  42201
  Copyright terms: Public domain W3C validator