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  3851  dfss2  3923  solin  5558  xpidtr  6075  f1ssres  6731  fvn0ssdmfun  7012  f1veqaeq  7197  f1opw  7609  resf1extb  7874  fprlem1  8240  ixpn0  8864  domunsncan  9001  phplem2  9129  php3  9133  infsupprpr  9415  frrlem15  9672  dfac9  10050  ltxrlt  11204  znegcl  12528  zltaddlt1le  13426  injresinj  13709  fsuppmapnn0fiubex  13917  pfxccatin12lem3  14656  repswswrd  14708  oddnn02np1  16277  sumeven  16316  ncoprmgcdne1b  16579  dvdsprmpweqnn  16815  prmodvdslcmf  16977  sgrpass  18617  symgextf1  19318  fvcosymgeq  19326  ricgic  20410  zringndrg  21393  evlslem4  21999  scmatf1  22434  pmatcoe1fsupp  22604  t1sncld  23229  regsep  23237  nrmsep3  23258  cmpsublem  23302  ufilss  23808  fclscf  23928  ncvsprp  25068  ncvsm1  25070  ncvsdif  25071  ncvspi  25072  ncvspds  25077  mblsplit  25449  mbfdm  25543  fta1glem1  26089  aaliou2  26264  dvloglem  26573  lgsqrlem4  27276  2sqnn0  27365  ausgrusgrb  29128  fusgredgfi  29288  vtxdumgrval  29450  vtxdginducedm1lem4  29506  umgrn1cycl  29770  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  0spth  30088  eucrctshift  30205  frcond1  30228  2pthfrgr  30246  frgrncvvdeqlem7  30267  frgrncvvdeq  30271  frgrwopreglem3  30276  frgrwopreglem5lem  30282  frgr2wwlk1  30291  numclwwlk1lem2f1  30319  hhcms  31165  stcltr1i  32236  bnj570  34871  bnj1145  34959  bnj1398  35000  bnj1442  35015  sconnpht  35201  fmla1  35359  goalrlem  35368  goalr  35369  satfv0fvfmla0  35385  fununiq  35741  rdgprc0  35766  bj-substw  36695  bj-opelresdm  37118  poimirlem25  37624  funressnfv  47028  funressnvmo  47030  euoreqb  47094  fcdmvafv2v  47221  dfatbrafv2b  47230  prproropf1olem4  47491  lighneallem2  47591  grlimgrtrilem2  47987  pgnioedg1  48093  pgnioedg2  48094  pgnioedg3  48095  pgnioedg4  48096  pgnioedg5  48097  pgnbgreunbgrlem2lem1  48099  pgnbgreunbgrlem2lem2  48100  pgnbgreunbgrlem2lem3  48101  pgnbgreunbgrlem5lem1  48105  pgnbgreunbgrlem5lem2  48106  pgnbgreunbgrlem5lem3  48107  lindslinindsimp1  48443  fullthinc  49436