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

Theorem simplbiim 508
 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 500 . 2 (𝜑𝜒)
3 simplbiim.2 . 2 (𝜒𝜃)
42, 3syl 17 1 (𝜑𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399 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  df-an 400 This theorem is referenced by:  2reu1  3826  invdisjrab  5017  solin  5463  xpidtr  5950  elpredim  6131  funimaexg  6413  f1ssres  6560  fvn0ssdmfun  6824  f1veqaeq  6998  f1opw  7387  ixpn0  8484  domunsncan  8607  phplem4  8690  php3  8694  infsupprpr  8959  dfac9  9554  ltxrlt  10707  znegcl  12012  zltaddlt1le  12890  injresinj  13160  fsuppmapnn0fiubex  13362  pfxccatin12lem3  14092  repswswrd  14144  oddnn02np1  15696  sumeven  15735  ncoprmgcdne1b  15991  dvdsprmpweqnn  16218  prmodvdslcmf  16380  sgrpass  17906  symgextf1  18549  fvcosymgeq  18557  ricgic  19502  zringndrg  20191  evlslem4  20757  scmatf1  21150  pmatcoe1fsupp  21320  t1sncld  21945  regsep  21953  nrmsep3  21974  cmpsublem  22018  ufilss  22524  fclscf  22644  ncvsprp  23771  ncvsm1  23773  ncvsdif  23774  ncvspi  23775  ncvspds  23780  mblsplit  24150  mbfdm  24244  fta1glem1  24780  aaliou2  24950  dvloglem  25253  lgsqrlem4  25947  2sqnn0  26036  ausgrusgrb  26972  fusgredgfi  27129  vtxdumgrval  27290  vtxdginducedm1lem4  27346  umgrn1cycl  27607  hashecclwwlkn1  27876  umgrhashecclwwlk  27877  0spth  27925  eucrctshift  28042  frcond1  28065  2pthfrgr  28083  frgrncvvdeqlem7  28104  frgrncvvdeq  28108  frgrwopreglem3  28113  frgrwopreglem5lem  28119  frgr2wwlk1  28128  numclwwlk1lem2f1  28156  hhcms  29000  stcltr1i  30071  bnj570  32323  bnj1145  32411  bnj1398  32452  bnj1442  32467  sconnpht  32625  fmla1  32783  goalrlem  32792  goalr  32793  satfv0fvfmla0  32809  fununiq  33161  rdgprc0  33187  fprlem1  33286  frrlem15  33291  bj-substw  34209  bj-opelresdm  34600  poimirlem25  35122  funressnfv  43696  funressnvmo  43698  euoreqb  43726  frnvafv2v  43853  dfatbrafv2b  43862  prproropf1olem4  44084  lighneallem2  44185  lindslinindsimp1  44925
 Copyright terms: Public domain W3C validator