Theorem simplbiim 505

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  2reu1  3890  invdisjrab  5133  solin  5612  xpidtr  6120  funimaexgOLD  6632  f1ssres  6792  fvn0ssdmfun  7073  f1veqaeq  7252  f1opw  7658  fprlem1  8281  ixpn0  8920  domunsncan  9068  phplem2  9204  php3  9208  phplem4OLD  9216  php3OLD  9220  infsupprpr  9495  frrlem15  9748  dfac9  10127  ltxrlt  11280  znegcl  12593  zltaddlt1le  13478  injresinj  13749  fsuppmapnn0fiubex  13953  pfxccatin12lem3  14678  repswswrd  14730  oddnn02np1  16287  sumeven  16326  ncoprmgcdne1b  16583  dvdsprmpweqnn  16814  prmodvdslcmf  16976  sgrpass  18612  symgextf1  19283  fvcosymgeq  19291  ricgic  20278  zringndrg  21029  evlslem4  21628  scmatf1  22024  pmatcoe1fsupp  22194  t1sncld  22821  regsep  22829  nrmsep3  22850  cmpsublem  22894  ufilss  23400  fclscf  23520  ncvsprp  24660  ncvsm1  24662  ncvsdif  24663  ncvspi  24664  ncvspds  24669  mblsplit  25040  mbfdm  25134  fta1glem1  25674  aaliou2  25844  dvloglem  26147  lgsqrlem4  26841  2sqnn0  26930  ausgrusgrb  28414  fusgredgfi  28571  vtxdumgrval  28732  vtxdginducedm1lem4  28788  umgrn1cycl  29050  hashecclwwlkn1  29319  umgrhashecclwwlk  29320  0spth  29368  eucrctshift  29485  frcond1  29508  2pthfrgr  29526  frgrncvvdeqlem7  29547  frgrncvvdeq  29551  frgrwopreglem3  29556  frgrwopreglem5lem  29562  frgr2wwlk1  29571  numclwwlk1lem2f1  29599  hhcms  30443  stcltr1i  31514  bnj570  33904  bnj1145  33992  bnj1398  34033  bnj1442  34048  sconnpht  34208  fmla1  34366  goalrlem  34375  goalr  34376  satfv0fvfmla0  34392  fununiq  34728  rdgprc0  34753  bj-substw  35588  bj-opelresdm  36014  poimirlem25  36501  funressnfv  45739  funressnvmo  45741  euoreqb  45803  fcdmvafv2v  45930  dfatbrafv2b  45939  prproropf1olem4  46160  lighneallem2  46260  lindslinindsimp1  47091  fullthinc  47619