Theorem simplbiim 504

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  2reu1  3897  dfss2  3969  solin  5619  xpidtr  6142  funimaexgOLD  6654  f1ssres  6811  fvn0ssdmfun  7094  f1veqaeq  7277  f1opw  7689  resf1extb  7956  fprlem1  8325  ixpn0  8970  domunsncan  9112  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  infsupprpr  9544  frrlem15  9797  dfac9  10177  ltxrlt  11331  znegcl  12652  zltaddlt1le  13545  injresinj  13827  fsuppmapnn0fiubex  14033  pfxccatin12lem3  14770  repswswrd  14822  oddnn02np1  16385  sumeven  16424  ncoprmgcdne1b  16687  dvdsprmpweqnn  16923  prmodvdslcmf  17085  sgrpass  18738  symgextf1  19439  fvcosymgeq  19447  ricgic  20507  zringndrg  21479  evlslem4  22100  scmatf1  22537  pmatcoe1fsupp  22707  t1sncld  23334  regsep  23342  nrmsep3  23363  cmpsublem  23407  ufilss  23913  fclscf  24033  ncvsprp  25186  ncvsm1  25188  ncvsdif  25189  ncvspi  25190  ncvspds  25195  mblsplit  25567  mbfdm  25661  fta1glem1  26207  aaliou2  26382  dvloglem  26690  lgsqrlem4  27393  2sqnn0  27482  ausgrusgrb  29182  fusgredgfi  29342  vtxdumgrval  29504  vtxdginducedm1lem4  29560  umgrn1cycl  29827  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  0spth  30145  eucrctshift  30262  frcond1  30285  2pthfrgr  30303  frgrncvvdeqlem7  30324  frgrncvvdeq  30328  frgrwopreglem3  30333  frgrwopreglem5lem  30339  frgr2wwlk1  30348  numclwwlk1lem2f1  30376  hhcms  31222  stcltr1i  32293  bnj570  34919  bnj1145  35007  bnj1398  35048  bnj1442  35063  sconnpht  35234  fmla1  35392  goalrlem  35401  goalr  35402  satfv0fvfmla0  35418  fununiq  35769  rdgprc0  35794  bj-substw  36723  bj-opelresdm  37146  poimirlem25  37652  funressnfv  47055  funressnvmo  47057  euoreqb  47121  fcdmvafv2v  47248  dfatbrafv2b  47257  prproropf1olem4  47493  lighneallem2  47593  grlimgrtrilem2  47962  lindslinindsimp1  48374  fullthinc  49099