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

Theorem imbi2i 303
Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)
Hypothesis
Ref Expression
bi.a  |-  ( ph  <->  ps )
Assertion
Ref Expression
imbi2i  |-  ( ( ch  ->  ph )  <->  ( ch  ->  ps ) )

Proof of Theorem imbi2i
StepHypRef Expression
1 bi.a . . 3  |-  ( ph  <->  ps )
21a1i 10 . 2  |-  ( ch 
->  ( ph  <->  ps )
)
32pm5.74i 236 1  |-  ( ( ch  ->  ph )  <->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi12i  316  iman  413  pm4.14  561  nan  563  pm5.32  617  anidmdbi  627  imimorb  847  pm5.6  878  exp3acom23g  1361  19.36  1819  sblim  2021  sban  2022  sbhb  2059  2sb6  2065  2sb6rf  2070  eu1  2177  moabs  2200  moanim  2212  2eu6  2241  r2alf  2591  r19.21t  2641  r19.35  2700  reu2  2966  reu8  2974  2reu5lem3  2985  ssconb  3322  ssin  3404  difin  3419  reldisj  3511  ssundif  3550  pwpw0  3779  pwsnALT  3838  unissb  3873  moabex  4248  dffr2  4374  dfepfr  4394  ssrel  4792  dffr3  5061  fncnv  5330  fun11  5331  dff13  5799  marypha2lem3  7206  dfsup2  7211  wemapso2lem  7281  inf2  7340  axinf2  7357  aceq1  7760  aceq0  7761  kmlem14  7805  dfackm  7808  zfac  8102  ac6n  8128  zfcndrep  8252  zfcndac  8257  axgroth6  8466  axgroth4  8470  grothprim  8472  prime  10108  raluz2  10284  rpnnen2  12520  isprm2  12782  isprm4  12784  pgpfac1  15331  pgpfac  15335  isirred2  15499  isclo2  16841  lmres  17044  ist1-2  17091  is1stc2  17184  alexsubALTlem3  17759  itg2cn  19134  ellimc3  19245  plydivex  19693  vieta1  19708  dchrelbas2  20492  nmobndseqi  21373  nmobndseqiOLD  21374  cvnbtwn3  22884  elat2  22936  ballotlemfc0  23067  ballotlemfcc  23068  bisimpd  23136  funcnvmptOLD  23249  funcnvmpt  23250  xrofsup  23270  disjrdx  23385  esumpcvgval  23461  esumcvg  23469  axinfprim  24067  dfon2lem9  24217  dffr4  24252  dffun10  24523  df3nandALT1  24906  df3nandALT2  24907  ltl4ev  25094  elicc3  26330  dfcon2OLD  26355  filnetlem4  26432  raldifsni  26855  dford4  27224  pm10.541  27664  pm13.196a  27716  2sbc6g  27717  wallispilem4  27919  wallispi2lem1  27922  rmoanim  28059  impexp3a  28573  bnj1098  29130  bnj1533  29199  bnj121  29217  bnj124  29218  bnj130  29221  bnj153  29227  bnj207  29228  bnj611  29265  bnj864  29269  bnj865  29270  bnj1000  29288  bnj978  29296  bnj1021  29311  bnj1047  29318  bnj1049  29319  bnj1090  29324  bnj1110  29327  bnj1128  29335  bnj1145  29338  bnj1171  29345  bnj1172  29346  bnj1174  29348  bnj1176  29350  bnj1280  29365  sblimNEW7  29542  sbanNEW7  29543  sbhbwAUX7  29578  2sb6NEW7  29581  sbhbOLD7  29714  2sb6rfOLD7  29718  a12peros  29743  lcvnbtwn3  29840  isat3  30119  cdleme25cv  31169  cdlemefrs29bpre0  31207  cdlemk35  31723
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator