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  3840  invdisjrab  5073  solin  5546  xpidtr  6050  funimaexgOLD  6558  f1ssres  6716  fvn0ssdmfun  6992  f1veqaeq  7170  f1opw  7567  fprlem1  8165  ixpn0  8768  domunsncan  8916  phplem2  9052  php3  9056  phplem4OLD  9064  php3OLD  9068  infsupprpr  9340  frrlem15  9593  dfac9  9972  ltxrlt  11125  znegcl  12435  zltaddlt1le  13317  injresinj  13588  fsuppmapnn0fiubex  13792  pfxccatin12lem3  14524  repswswrd  14576  oddnn02np1  16136  sumeven  16175  ncoprmgcdne1b  16432  dvdsprmpweqnn  16663  prmodvdslcmf  16825  sgrpass  18458  symgextf1  19105  fvcosymgeq  19113  ricgic  20065  zringndrg  20773  evlslem4  21367  scmatf1  21763  pmatcoe1fsupp  21933  t1sncld  22560  regsep  22568  nrmsep3  22589  cmpsublem  22633  ufilss  23139  fclscf  23259  ncvsprp  24399  ncvsm1  24401  ncvsdif  24402  ncvspi  24403  ncvspds  24408  mblsplit  24779  mbfdm  24873  fta1glem1  25413  aaliou2  25583  dvloglem  25886  lgsqrlem4  26580  2sqnn0  26669  ausgrusgrb  27671  fusgredgfi  27828  vtxdumgrval  27989  vtxdginducedm1lem4  28045  umgrn1cycl  28308  hashecclwwlkn1  28577  umgrhashecclwwlk  28578  0spth  28626  eucrctshift  28743  frcond1  28766  2pthfrgr  28784  frgrncvvdeqlem7  28805  frgrncvvdeq  28809  frgrwopreglem3  28814  frgrwopreglem5lem  28820  frgr2wwlk1  28829  numclwwlk1lem2f1  28857  hhcms  29701  stcltr1i  30772  bnj570  33024  bnj1145  33112  bnj1398  33153  bnj1442  33168  sconnpht  33330  fmla1  33488  goalrlem  33497  goalr  33498  satfv0fvfmla0  33514  fununiq  33874  rdgprc0  33900  bj-substw  34978  bj-opelresdm  35388  poimirlem25  35874  funressnfv  44802  funressnvmo  44804  euoreqb  44866  fcdmvafv2v  44993  dfatbrafv2b  45002  prproropf1olem4  45223  lighneallem2  45323  lindslinindsimp1  46063  fullthinc  46592