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

Theorem imbi2i 339
 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 274 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  jcndOLD  340  iman  405  anidmdbi  569  pm5.32  577  pm4.14  806  nan  828  imimorb  948  pm5.6  999  nannan  1488  alimex  1832  19.36v  1994  2sb6  2091  sbrimvlem  2098  sbal  2163  19.36  2230  sbn  2283  sbanOLD  2308  sblim  2311  sbanvOLD  2319  sbhb  2540  sbanALT  2586  dfmo  2657  eu1  2671  cbvabw  2867  ralbii  3133  r19.21v  3142  r2allem  3165  r3al  3167  r19.21t  3178  rspc2gv  3580  reu2  3664  reu8  3672  2reu5lem3  3696  rmoanim  3823  rmoanimALT  3824  dfdif3  4042  ssconb  4065  ssin  4157  difin  4188  reldisj  4359  reldisjOLD  4360  ssundif  4391  reuprg0  4598  raldifsni  4688  pwpw0  4706  pwsnOLD  4794  unissb  4833  moabex  5317  dffr2  5485  dfepfr  5505  ssrel2  5624  dffr3  5930  opreu2reurex  6116  dffr4  6135  fncnv  6400  fun11  6401  dff13  6996  marypha2lem3  8892  dfsup2  8899  wemapsolem  9005  inf2  9077  axinf2  9094  aceq1  9535  aceq0  9536  kmlem14  9581  dfackm  9584  zfac  9878  ac6n  9903  zfcndrep  10032  zfcndac  10037  axgroth6  10246  axgroth4  10250  grothprim  10252  prime  12058  raluz2  12292  fsuppmapnn0ub  13365  mptnn0fsuppr  13369  brtrclfv  14360  rpnnen2lem12  15577  isprm2  16023  isprm4  16025  pgpfac1  19203  pgpfac  19207  isirred2  19455  pmatcollpw2lem  21396  isclo2  21707  lmres  21919  ist1-2  21966  is1stc2  22061  alexsubALTlem3  22668  itg2cn  24381  ellimc3  24496  plydivex  24907  vieta1  24922  dchrelbas2  25835  nmobndseqi  28576  nmobndseqiALT  28577  cvnbtwn3  30085  elat2  30137  inpr0  30318  ssrelf  30393  isarchi2  30883  archiabl  30896  islinds5  31002  esumcvgre  31496  signstfvneq0  31988  hashreprin  32037  breprexp  32050  bnj1098  32201  bnj1533  32270  bnj121  32288  bnj124  32289  bnj130  32292  bnj153  32298  bnj207  32299  bnj611  32336  bnj864  32340  bnj865  32341  bnj1000  32359  bnj978  32367  bnj1021  32384  bnj1047  32391  bnj1049  32392  bnj1090  32397  bnj1110  32400  bnj1128  32408  bnj1145  32411  bnj1171  32418  bnj1172  32419  bnj1174  32421  bnj1176  32423  bnj1280  32438  axinfprim  33081  dfon2lem9  33185  conway  33413  dffun10  33524  elicc3  33814  filnetlem4  33878  df3nandALT1  33896  df3nandALT2  33897  bj-ssbeq  34139  bj-ax12ssb  34144  bj-sbnf  34319  pibt2  34874  wl-dfralsb  35042  wl-dfrexex  35055  wl-dfrexsb  35056  wl-dfrmosb  35058  poimirlem30  35127  inxpssidinxp  35773  lcvnbtwn3  36364  isat3  36643  cdleme25cv  37694  cdlemefrs29bpre0  37732  cdlemk35  38248  metakunt6  39395  metakunt24  39413  2xp3dxp2ge1d  39427  sn-axrep5v  39440  dford4  40034  ifpidg  40263  ifpid1g  40266  ifpim23g  40267  ifpororb  40277  ifpbibib  40282  elinintrab  40341  undmrnresiss  40368  cotrintab  40378  elintima  40418  frege60b  40670  frege91  40719  frege97  40725  frege98  40726  dffrege99  40727  frege109  40737  frege110  40738  frege131  40759  frege133  40761  ntrneiiso  40858  int-sqdefd  40951  int-sqgeq0d  40956  ismnuprim  41066  pm10.541  41135  pm13.196a  41182  2sbc6g  41183  expcomdg  41270  impexpd  41283  supxrleubrnmptf  42151  fsummulc1f  42273  fsumiunss  42278  fnlimfvre2  42380  limsupreuz  42440  limsupvaluz2  42441  lmbr3v  42448  dvmptmulf  42640  dvmptfprodlem  42647  sge0ltfirpmpt2  43126  hoidmv1le  43294  hoidmvle  43300  vonioolem2  43381  smflimlem3  43467  ldepslinc  44977  setrec1lem2  45277  setrec2  45284  sbidd-misc  45304
 Copyright terms: Public domain W3C validator