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  3848  dfss2  3920  solin  5551  xpidtr  6069  f1ssres  6726  fvn0ssdmfun  7007  f1veqaeq  7190  f1opw  7602  resf1extb  7864  fprlem1  8230  ixpn0  8854  domunsncan  8990  phplem2  9114  php3  9118  infsupprpr  9390  frrlem15  9647  dfac9  10025  ltxrlt  11180  znegcl  12504  zltaddlt1le  13402  injresinj  13688  fsuppmapnn0fiubex  13896  pfxccatin12lem3  14636  repswswrd  14688  oddnn02np1  16256  sumeven  16295  ncoprmgcdne1b  16558  dvdsprmpweqnn  16794  prmodvdslcmf  16956  sgrpass  18630  symgextf1  19331  fvcosymgeq  19339  ricgic  20420  zringndrg  21403  evlslem4  22009  scmatf1  22444  pmatcoe1fsupp  22614  t1sncld  23239  regsep  23247  nrmsep3  23268  cmpsublem  23312  ufilss  23818  fclscf  23938  ncvsprp  25077  ncvsm1  25079  ncvsdif  25080  ncvspi  25081  ncvspds  25086  mblsplit  25458  mbfdm  25552  fta1glem1  26098  aaliou2  26273  dvloglem  26582  lgsqrlem4  27285  2sqnn0  27374  ausgrusgrb  29141  fusgredgfi  29301  vtxdumgrval  29463  vtxdginducedm1lem4  29519  umgrn1cycl  29783  hashecclwwlkn1  30052  umgrhashecclwwlk  30053  0spth  30101  eucrctshift  30218  frcond1  30241  2pthfrgr  30259  frgrncvvdeqlem7  30280  frgrncvvdeq  30284  frgrwopreglem3  30289  frgrwopreglem5lem  30295  frgr2wwlk1  30304  numclwwlk1lem2f1  30332  hhcms  31178  stcltr1i  32249  bnj570  34912  bnj1145  35000  bnj1398  35041  bnj1442  35056  sconnpht  35261  fmla1  35419  goalrlem  35428  goalr  35429  satfv0fvfmla0  35445  fununiq  35801  rdgprc0  35826  bj-substw  36755  bj-opelresdm  37178  poimirlem25  37684  funressnfv  47073  funressnvmo  47075  euoreqb  47139  fcdmvafv2v  47266  dfatbrafv2b  47275  prproropf1olem4  47536  lighneallem2  47636  grlimgrtrilem2  48032  pgnioedg1  48138  pgnioedg2  48139  pgnioedg3  48140  pgnioedg4  48141  pgnioedg5  48142  pgnbgreunbgrlem2lem1  48144  pgnbgreunbgrlem2lem2  48145  pgnbgreunbgrlem2lem3  48146  pgnbgreunbgrlem5lem1  48150  pgnbgreunbgrlem5lem2  48151  pgnbgreunbgrlem5lem3  48152  lindslinindsimp1  48488  fullthinc  49481