Theorem simplbiim 507

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 499	. 2 ⊢ (𝜑 → 𝜒)
3		simplbiim.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  2reu1  3880  invdisjrab  5051  solin  5497  xpidtr  5981  elpredim  6159  funimaexg  6439  f1ssres  6581  fvn0ssdmfun  6841  f1veqaeq  7014  f1opw  7400  ixpn0  8493  domunsncan  8616  phplem4  8698  php3  8702  infsupprpr  8967  dfac9  9561  ltxrlt  10710  znegcl  12016  zltaddlt1le  12889  injresinj  13157  fsuppmapnn0fiubex  13359  pfxccatin12lem3  14093  repswswrd  14145  oddnn02np1  15696  sumeven  15737  ncoprmgcdne1b  15993  dvdsprmpweqnn  16220  prmodvdslcmf  16382  sgrpass  17906  symgextf1  18548  fvcosymgeq  18556  ricgic  19500  evlslem4  20287  zringndrg  20636  scmatf1  21139  pmatcoe1fsupp  21308  t1sncld  21933  regsep  21941  nrmsep3  21962  cmpsublem  22006  ufilss  22512  fclscf  22632  ncvsprp  23755  ncvsm1  23757  ncvsdif  23758  ncvspi  23759  ncvspds  23764  mblsplit  24132  mbfdm  24226  fta1glem1  24758  aaliou2  24928  dvloglem  25230  lgsqrlem4  25924  2sqnn0  26013  ausgrusgrb  26949  fusgredgfi  27106  vtxdumgrval  27267  vtxdginducedm1lem4  27323  umgrn1cycl  27584  hashecclwwlkn1  27855  umgrhashecclwwlk  27856  0spth  27904  eucrctshift  28021  frcond1  28044  2pthfrgr  28062  frgrncvvdeqlem7  28083  frgrncvvdeq  28087  frgrwopreglem3  28092  frgrwopreglem5lem  28098  frgr2wwlk1  28107  numclwwlk1lem2f1  28135  hhcms  28979  stcltr1i  30050  bnj570  32177  bnj1145  32265  bnj1398  32306  bnj1442  32321  sconnpht  32476  fmla1  32634  goalrlem  32643  goalr  32644  satfv0fvfmla0  32660  fununiq  33012  fprlem1  33137  frrlem15  33142  bj-opelresdm  34436  poimirlem25  34916  funressnfv  43277  funressnvmo  43279  euoreqb  43307  frnvafv2v  43434  dfatbrafv2b  43443  prproropf1olem4  43667  lighneallem2  43770  lindslinindsimp1  44511