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  3848  dfss2  3920  solin  5594  xpidtr  6120  f1ssres  6784  fvn0ssdmfun  7071  f1veqaeq  7257  f1opw  7674  resf1extb  7935  fprlem1  8303  ixpn0  8941  domunsncan  9079  phplem2  9203  php3  9207  infsupprpr  9480  frrlem15  9743  dfac9  10143  ltxrlt  11308  znegcl  12657  zltaddlt1le  13562  injresinj  13851  fsuppmapnn0fiubex  14060  pfxccatin12lem3  14805  repswswrd  14859  oddnn02np1  16444  sumeven  16483  ncoprmgcdne1b  16746  dvdsprmpweqnn  16983  prmodvdslcmf  17145  sgrpass  18833  symgextf1  19554  fvcosymgeq  19562  ricgic  20672  zringndrg  21687  evlslem4  22298  scmatf1  22759  pmatcoe1fsupp  22932  t1sncld  23557  regsep  23565  nrmsep3  23586  cmpsublem  23630  ufilss  24137  fclscf  24257  ncvsprp  25386  ncvsm1  25388  ncvsdif  25389  ncvspi  25390  ncvspds  25395  mblsplit  25766  mbfdm  25860  fta1glem1  26400  aaliou2  26583  dvloglem  26893  lgsqrlem4  27593  2sqnn0  27682  ausgrusgrb  29633  fusgredgfi  29793  vtxdumgrval  29954  vtxdginducedm1lem4  30010  umgrn1cycl  30283  hashecclwwlkn1  30555  umgrhashecclwwlk  30556  0spth  30604  eucrctshift  30731  frcond1  30754  2pthfrgr  30772  frgrncvvdeqlem7  30793  frgrncvvdeq  30797  frgrwopreglem3  30802  frgrwopreglem5lem  30808  frgr2wwlk1  30817  numclwwlk1lem2f1  30845  hhcms  31692  stcltr1i  32763  chpssati  32852  bnj570  35422  bnj1145  35510  bnj1398  35551  bnj1442  35566  sconnpht  35816  fmla1  35974  goalrlem  35983  goalr  35984  satfv0fvfmla0  36000  fununiq  36356  rdgprc0  36378  bj-substw  37466  bj-opelresdm  37905  poimirlem25  38402  funressnfv  47939  funressnvmo  47941  euoreqb  48005  fcdmvafv2v  48132  dfatbrafv2b  48141  prproropf1olem4  48414  lighneallem2  48517  grlimgrtrilem2  48926  pgnioedg1  49032  pgnioedg2  49033  pgnioedg3  49034  pgnioedg4  49035  pgnioedg5  49036  pgnbgreunbgrlem2lem1  49038  pgnbgreunbgrlem2lem2  49039  pgnbgreunbgrlem2lem3  49040  pgnbgreunbgrlem5lem1  49044  pgnbgreunbgrlem5lem2  49045  pgnbgreunbgrlem5lem3  49046  lindslinindsimp1  49395  fullthinc  50384