MPE Home 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  601  nan  603  pm5.32  669  anidmdbi  679  imimorb  939  pm5.6  971  nannan  1491  alimex  1798  19.36v  1960  19.36  2136  sblim  2425  sban  2427  sbhb  2466  2sb6  2472  mo2v  2505  moabs  2530  eu1  2539  r2allem  2966  r3al  2969  r19.21t  2984  r19.21v  2989  ralbii  3009  r19.35  3113  rspc2gv  3352  reu2  3427  reu8  3435  2reu5lem3  3448  ssconb  3776  ssin  3868  difin  3894  reldisj  4053  ssundif  4085  raldifsni  4357  pwpw0  4376  pwsnALT  4461  unissb  4501  moabex  4957  dffr2  5108  dfepfr  5128  ssrelOLD  5242  ssrel2  5244  dffr3  5533  dffr4  5734  fncnv  6000  fun11  6001  dff13  6552  marypha2lem3  8384  dfsup2  8391  wemapsolem  8496  inf2  8558  axinf2  8575  aceq1  8978  aceq0  8979  kmlem14  9023  dfackm  9026  zfac  9320  ac6n  9345  zfcndrep  9474  zfcndac  9479  axgroth6  9688  axgroth4  9692  grothprim  9694  prime  11496  raluz2  11775  fsuppmapnn0ub  12835  mptnn0fsuppr  12839  brtrclfv  13787  rpnnen2lem12  14998  isprm2  15442  isprm4  15444  pgpfac1  18525  pgpfac  18529  isirred2  18747  pmatcollpw2lem  20630  isclo2  20940  lmres  21152  ist1-2  21199  is1stc2  21293  alexsubALTlem3  21900  itg2cn  23575  ellimc3  23688  plydivex  24097  vieta1  24112  dchrelbas2  25007  nmobndseqi  27762  nmobndseqiALT  27763  cvnbtwn3  29275  elat2  29327  ssrelf  29553  funcnvmptOLD  29595  isarchi2  29867  archiabl  29880  esumcvgre  30281  signstfvneq0  30777  hashreprin  30826  breprexp  30839  bnj1098  30980  bnj1533  31048  bnj121  31066  bnj124  31067  bnj130  31070  bnj153  31076  bnj207  31077  bnj611  31114  bnj864  31118  bnj865  31119  bnj1000  31137  bnj978  31145  bnj1021  31160  bnj1047  31167  bnj1049  31168  bnj1090  31173  bnj1110  31176  bnj1128  31184  bnj1145  31187  bnj1171  31194  bnj1172  31195  bnj1174  31197  bnj1176  31199  bnj1280  31214  axinfprim  31709  dfon2lem9  31820  conway  32035  dffun10  32146  elicc3  32436  filnetlem4  32501  df3nandALT1  32521  df3nandALT2  32522  bj-ssbeq  32752  bj-ssb0  32753  bj-ax12ssb  32760  bj-ssbn  32766  bj-sbnf  32953  wl-nannan  33428  poimirlem30  33569  inxpssidinxp  34227  lcvnbtwn3  34633  isat3  34912  cdleme25cv  35963  cdlemefrs29bpre0  36001  cdlemk35  36517  dford4  37913  ifpidg  38153  ifpid1g  38156  ifpim23g  38157  ifpororb  38167  ifpbibib  38172  elinintrab  38200  undmrnresiss  38227  cotrintab  38238  elintima  38262  frege60b  38516  frege91  38565  frege97  38571  frege98  38572  dffrege99  38573  frege109  38583  frege110  38584  frege131  38605  frege133  38607  ntrneiiso  38706  int-sqdefd  38801  int-sqgeq0d  38806  pm10.541  38883  pm13.196a  38932  2sbc6g  38933  expcomdg  39023  impexpd  39036  jcn  39519  supxrleubrnmptf  39993  fsummulc1f  40120  fsumiunss  40125  fnlimfvre2  40227  limsupreuz  40287  limsupvaluz2  40288  lmbr3v  40295  dvmptmulf  40470  dvmptfprodlem  40477  sge0ltfirpmpt2  40961  hoidmv1le  41129  hoidmvle  41135  vonioolem2  41216  smflimlem3  41302  rmoanim  41500  ldepslinc  42623  setrec1lem2  42760  setrec2  42767  sbidd-misc  42788
  Copyright terms: Public domain W3C validator