Theorem simplbiim 514

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

Step	Hyp	Ref	Expression
1		simplbiim.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	simprbi 503	. 2 ⊢ (𝜑 → 𝜒)
3		simplbiim.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 18	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  2reu1  3849  dfss2  4097  solin  5590  xpidtr  6128  fununiq  6575  f1ssres  6809  fvn0ssdmfun  7098  f1veqaeq  7283  f1opw  7701  resf1extb  7970  fprlem1  8346  ixpn0  8986  domunsncan  9124  phplem2  9248  php3  9252  infsupprpr  9525  frrlem15  9788  dfac9  10242  ltxrlt  11407  znegcl  12758  zltaddlt1le  13663  injresinj  13953  fsuppmapnn0fiubex  14162  pfxccatin12lem3  14909  repswswrd  14963  oddnn02np1  16547  sumeven  16586  ncoprmgcdne1b  16854  dvdsprmpweqnn  17092  prmodvdslcmf  17254  sgrpass  18943  symgextf1  19665  fvcosymgeq  19673  ricgic  20785  zringndrg  21804  evlslem4  22415  scmatf1  22876  pmatcoe1fsupp  23049  t1sncld  23674  regsep  23682  nrmsep3  23703  cmpsublem  23747  ufilss  24254  fclscf  24374  ncvsprp  25503  ncvsm1  25505  ncvsdif  25506  ncvspi  25507  ncvspds  25512  mblsplit  25883  mbfdm  25977  fta1glem1  26516  aaliou2  26697  dvloglem  27006  lgsqrlem4  27706  2sqnn0  27795  ausgrusgrb  29776  fusgredgfi  29936  vtxdumgrval  30097  vtxdginducedm1lem4  30153  umgrn1cycl  30426  hashecclwwlkn1  30698  umgrhashecclwwlk  30699  0spth  30747  eucrctshift  30874  frcond1  30897  2pthfrgr  30915  frgrncvvdeqlem7  30936  frgrncvvdeq  30940  frgrwopreglem3  30945  frgrwopreglem5lem  30951  frgr2wwlk1  30960  numclwwlk1lem2f1  30988  hhcms  31835  stcltr1i  32906  chpssati  32995  bnj570  35605  bnj1145  35693  bnj1398  35734  bnj1442  35749  scottidm  35841  sconnpht  36161  fmla1  36319  goalrlem  36328  goalr  36329  satfv0fvfmla0  36345  rdgprc0  36733  bj-substw  37805  bj-opelresdm  38258  poimirlem25  38755  funressnfv  48318  funressnvmo  48320  euoreqb  48385  fcdmvafv2v  48511  dfatbrafv2b  48520  prproropf1olem4  48793  lighneallem2  48896  grlimgrtrilem2  49305  pgnioedg1  49411  pgnioedg2  49412  pgnioedg3  49413  pgnioedg4  49414  pgnioedg5  49415  pgnbgreunbgrlem2lem1  49417  pgnbgreunbgrlem2lem2  49418  pgnbgreunbgrlem2lem3  49419  pgnbgreunbgrlem5lem1  49423  pgnbgreunbgrlem5lem2  49424  pgnbgreunbgrlem5lem3  49425  lindslinindsimp1  49774  fullthinc  50790