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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  2reu1  3826  invdisjrab  5056  solin  5519  xpidtr  6016  funimaexg  6504  f1ssres  6662  fvn0ssdmfun  6934  f1veqaeq  7111  f1opw  7503  fprlem1  8087  ixpn0  8676  domunsncan  8812  phplem4  8895  php3  8899  infsupprpr  9193  frrlem15  9446  dfac9  9823  ltxrlt  10976  znegcl  12285  zltaddlt1le  13166  injresinj  13436  fsuppmapnn0fiubex  13640  pfxccatin12lem3  14373  repswswrd  14425  oddnn02np1  15985  sumeven  16024  ncoprmgcdne1b  16283  dvdsprmpweqnn  16514  prmodvdslcmf  16676  sgrpass  18296  symgextf1  18944  fvcosymgeq  18952  ricgic  19905  zringndrg  20602  evlslem4  21194  scmatf1  21588  pmatcoe1fsupp  21758  t1sncld  22385  regsep  22393  nrmsep3  22414  cmpsublem  22458  ufilss  22964  fclscf  23084  ncvsprp  24221  ncvsm1  24223  ncvsdif  24224  ncvspi  24225  ncvspds  24230  mblsplit  24601  mbfdm  24695  fta1glem1  25235  aaliou2  25405  dvloglem  25708  lgsqrlem4  26402  2sqnn0  26491  ausgrusgrb  27438  fusgredgfi  27595  vtxdumgrval  27756  vtxdginducedm1lem4  27812  umgrn1cycl  28073  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  0spth  28391  eucrctshift  28508  frcond1  28531  2pthfrgr  28549  frgrncvvdeqlem7  28570  frgrncvvdeq  28574  frgrwopreglem3  28579  frgrwopreglem5lem  28585  frgr2wwlk1  28594  numclwwlk1lem2f1  28622  hhcms  29466  stcltr1i  30537  bnj570  32785  bnj1145  32873  bnj1398  32914  bnj1442  32929  sconnpht  33091  fmla1  33249  goalrlem  33258  goalr  33259  satfv0fvfmla0  33275  fununiq  33649  rdgprc0  33675  bj-substw  34831  bj-opelresdm  35243  poimirlem25  35729  funressnfv  44424  funressnvmo  44426  euoreqb  44488  frnvafv2v  44615  dfatbrafv2b  44624  prproropf1olem4  44846  lighneallem2  44946  lindslinindsimp1  45686  fullthinc  46215