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  3830  invdisjrab  5060  solin  5528  xpidtr  6027  funimaexg  6520  f1ssres  6678  fvn0ssdmfun  6952  f1veqaeq  7130  f1opw  7525  fprlem1  8116  ixpn0  8718  domunsncan  8859  phplem2  8991  php3  8995  phplem4OLD  9003  php3OLD  9007  infsupprpr  9263  frrlem15  9515  dfac9  9892  ltxrlt  11045  znegcl  12355  zltaddlt1le  13237  injresinj  13508  fsuppmapnn0fiubex  13712  pfxccatin12lem3  14445  repswswrd  14497  oddnn02np1  16057  sumeven  16096  ncoprmgcdne1b  16355  dvdsprmpweqnn  16586  prmodvdslcmf  16748  sgrpass  18381  symgextf1  19029  fvcosymgeq  19037  ricgic  19990  zringndrg  20690  evlslem4  21284  scmatf1  21680  pmatcoe1fsupp  21850  t1sncld  22477  regsep  22485  nrmsep3  22506  cmpsublem  22550  ufilss  23056  fclscf  23176  ncvsprp  24316  ncvsm1  24318  ncvsdif  24319  ncvspi  24320  ncvspds  24325  mblsplit  24696  mbfdm  24790  fta1glem1  25330  aaliou2  25500  dvloglem  25803  lgsqrlem4  26497  2sqnn0  26586  ausgrusgrb  27535  fusgredgfi  27692  vtxdumgrval  27853  vtxdginducedm1lem4  27909  umgrn1cycl  28172  hashecclwwlkn1  28441  umgrhashecclwwlk  28442  0spth  28490  eucrctshift  28607  frcond1  28630  2pthfrgr  28648  frgrncvvdeqlem7  28669  frgrncvvdeq  28673  frgrwopreglem3  28678  frgrwopreglem5lem  28684  frgr2wwlk1  28693  numclwwlk1lem2f1  28721  hhcms  29565  stcltr1i  30636  bnj570  32885  bnj1145  32973  bnj1398  33014  bnj1442  33029  sconnpht  33191  fmla1  33349  goalrlem  33358  goalr  33359  satfv0fvfmla0  33375  fununiq  33743  rdgprc0  33769  bj-substw  34904  bj-opelresdm  35316  poimirlem25  35802  funressnfv  44537  funressnvmo  44539  euoreqb  44601  frnvafv2v  44728  dfatbrafv2b  44737  prproropf1olem4  44958  lighneallem2  45058  lindslinindsimp1  45798  fullthinc  46327