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  3854  dfss2  3926  solin  5601  xpidtr  6127  f1ssres  6790  fvn0ssdmfun  7076  f1veqaeq  7261  f1opw  7679  resf1extb  7940  fprlem1  8306  ixpn0  8937  domunsncan  9075  phplem2  9199  php3  9203  infsupprpr  9476  frrlem15  9739  dfac9  10139  ltxrlt  11298  znegcl  12647  zltaddlt1le  13550  injresinj  13839  fsuppmapnn0fiubex  14048  pfxccatin12lem3  14793  repswswrd  14847  oddnn02np1  16431  sumeven  16470  ncoprmgcdne1b  16733  dvdsprmpweqnn  16970  prmodvdslcmf  17132  sgrpass  18812  symgextf1  19522  fvcosymgeq  19530  ricgic  20640  zringndrg  21655  evlslem4  22264  scmatf1  22725  pmatcoe1fsupp  22895  t1sncld  23520  regsep  23528  nrmsep3  23549  cmpsublem  23593  ufilss  24099  fclscf  24219  ncvsprp  25348  ncvsm1  25350  ncvsdif  25351  ncvspi  25352  ncvspds  25357  mblsplit  25728  mbfdm  25822  fta1glem1  26362  aaliou2  26540  dvloglem  26850  lgsqrlem4  27550  2sqnn0  27639  ausgrusgrb  29552  fusgredgfi  29712  vtxdumgrval  29873  vtxdginducedm1lem4  29929  umgrn1cycl  30193  hashecclwwlkn1  30465  umgrhashecclwwlk  30466  0spth  30514  eucrctshift  30631  frcond1  30654  2pthfrgr  30672  frgrncvvdeqlem7  30693  frgrncvvdeq  30697  frgrwopreglem3  30702  frgrwopreglem5lem  30708  frgr2wwlk1  30717  numclwwlk1lem2f1  30745  hhcms  31592  stcltr1i  32663  chpssati  32752  bnj570  35325  bnj1145  35413  bnj1398  35454  bnj1442  35469  sconnpht  35742  fmla1  35900  goalrlem  35909  goalr  35910  satfv0fvfmla0  35926  fununiq  36282  rdgprc0  36304  bj-substw  37391  bj-opelresdm  37830  poimirlem25  38337  funressnfv  47821  funressnvmo  47823  euoreqb  47887  fcdmvafv2v  48014  dfatbrafv2b  48023  prproropf1olem4  48296  lighneallem2  48399  grlimgrtrilem2  48808  pgnioedg1  48914  pgnioedg2  48915  pgnioedg3  48916  pgnioedg4  48917  pgnioedg5  48918  pgnbgreunbgrlem2lem1  48920  pgnbgreunbgrlem2lem2  48921  pgnbgreunbgrlem2lem3  48922  pgnbgreunbgrlem5lem1  48926  pgnbgreunbgrlem5lem2  48927  pgnbgreunbgrlem5lem3  48928  lindslinindsimp1  49278  fullthinc  50269