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  3905  dfss2  3980  solin  5622  xpidtr  6144  funimaexgOLD  6654  f1ssres  6811  fvn0ssdmfun  7093  f1veqaeq  7276  f1opw  7688  fprlem1  8323  ixpn0  8968  domunsncan  9110  phplem2  9242  php3  9246  phplem4OLD  9254  php3OLD  9258  infsupprpr  9541  frrlem15  9794  dfac9  10174  ltxrlt  11328  znegcl  12649  zltaddlt1le  13541  injresinj  13823  fsuppmapnn0fiubex  14029  pfxccatin12lem3  14766  repswswrd  14818  oddnn02np1  16381  sumeven  16420  ncoprmgcdne1b  16683  dvdsprmpweqnn  16918  prmodvdslcmf  17080  sgrpass  18750  symgextf1  19453  fvcosymgeq  19461  ricgic  20523  zringndrg  21496  evlslem4  22117  scmatf1  22552  pmatcoe1fsupp  22722  t1sncld  23349  regsep  23357  nrmsep3  23378  cmpsublem  23422  ufilss  23928  fclscf  24048  ncvsprp  25199  ncvsm1  25201  ncvsdif  25202  ncvspi  25203  ncvspds  25208  mblsplit  25580  mbfdm  25674  fta1glem1  26221  aaliou2  26396  dvloglem  26704  lgsqrlem4  27407  2sqnn0  27496  ausgrusgrb  29196  fusgredgfi  29356  vtxdumgrval  29518  vtxdginducedm1lem4  29574  umgrn1cycl  29836  hashecclwwlkn1  30105  umgrhashecclwwlk  30106  0spth  30154  eucrctshift  30271  frcond1  30294  2pthfrgr  30312  frgrncvvdeqlem7  30333  frgrncvvdeq  30337  frgrwopreglem3  30342  frgrwopreglem5lem  30348  frgr2wwlk1  30357  numclwwlk1lem2f1  30385  hhcms  31231  stcltr1i  32302  bnj570  34897  bnj1145  34985  bnj1398  35026  bnj1442  35041  sconnpht  35213  fmla1  35371  goalrlem  35380  goalr  35381  satfv0fvfmla0  35397  fununiq  35749  rdgprc0  35774  bj-substw  36704  bj-opelresdm  37127  poimirlem25  37631  funressnfv  46992  funressnvmo  46994  euoreqb  47058  fcdmvafv2v  47185  dfatbrafv2b  47194  prproropf1olem4  47430  lighneallem2  47530  grlimgrtrilem2  47897  lindslinindsimp1  48302  fullthinc  48845