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

Theorem simplbiim 505
Description: Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)
Hypotheses
Ref Expression
simplbiim.1 (𝜑 ↔ (𝜓𝜒))
simplbiim.2 (𝜒𝜃)
Assertion
Ref Expression
simplbiim (𝜑𝜃)

Proof of Theorem simplbiim
StepHypRef Expression
1 simplbiim.1 . . 3 (𝜑 ↔ (𝜓𝜒))
21simprbi 497 . 2 (𝜑𝜒)
3 simplbiim.2 . 2 (𝜒𝜃)
42, 3syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  2reu1  3885  invdisjrab  5049  solin  5497  xpidtr  5980  elpredim  6158  funimaexg  6437  f1ssres  6579  fvn0ssdmfun  6838  f1veqaeq  7009  f1opw  7391  ixpn0  8483  domunsncan  8606  phplem4  8688  php3  8692  infsupprpr  8957  dfac9  9551  ltxrlt  10700  znegcl  12006  zltaddlt1le  12880  injresinj  13148  fsuppmapnn0fiubex  13350  pfxccatin12lem3  14084  repswswrd  14136  oddnn02np1  15687  sumeven  15728  ncoprmgcdne1b  15984  dvdsprmpweqnn  16211  prmodvdslcmf  16373  sgrpass  17896  symgextf1  18469  fvcosymgeq  18477  ricgic  19421  evlslem4  20206  zringndrg  20553  scmatf1  21056  pmatcoe1fsupp  21225  t1sncld  21850  regsep  21858  nrmsep3  21879  cmpsublem  21923  ufilss  22429  fclscf  22549  ncvsprp  23671  ncvsm1  23673  ncvsdif  23674  ncvspi  23675  ncvspds  23680  mblsplit  24048  mbfdm  24142  fta1glem1  24674  aaliou2  24844  dvloglem  25144  lgsqrlem4  25839  2sqnn0  25928  ausgrusgrb  26864  fusgredgfi  27021  vtxdumgrval  27182  vtxdginducedm1lem4  27238  umgrn1cycl  27499  hashecclwwlkn1  27770  umgrhashecclwwlk  27771  0spth  27819  eucrctshift  27936  frcond1  27959  2pthfrgr  27977  frgrncvvdeqlem7  27998  frgrncvvdeq  28002  frgrwopreglem3  28007  frgrwopreglem5lem  28013  frgr2wwlk1  28022  numclwwlk1lem2f1  28050  hhcms  28894  stcltr1i  29965  bnj570  32063  bnj1145  32149  bnj1398  32190  bnj1442  32205  sconnpht  32360  fmla1  32518  goalrlem  32527  goalr  32528  satfv0fvfmla0  32544  fununiq  32896  fprlem1  33021  frrlem15  33026  bj-opelresdm  34316  poimirlem25  34784  funressnfv  43144  funressnvmo  43146  euoreqb  43174  frnvafv2v  43301  dfatbrafv2b  43310  prproropf1olem4  43500  lighneallem2  43603  lindslinindsimp1  44344
  Copyright terms: Public domain W3C validator