Theorem simplbiim 513

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 502	. 2 ⊢ (𝜑 → 𝜒)
3		simplbiim.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 18	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  2reu1  3853  dfss2  3925  solin  5587  xpidtr  6113  f1ssres  6773  fvn0ssdmfun  7059  f1veqaeq  7244  f1opw  7656  resf1extb  7919  fprlem1  8285  ixpn0  8916  domunsncan  9053  phplem2  9177  php3  9181  infsupprpr  9454  frrlem15  9717  dfac9  10108  ltxrlt  11268  znegcl  12620  zltaddlt1le  13523  injresinj  13811  fsuppmapnn0fiubex  14019  pfxccatin12lem3  14759  repswswrd  14811  oddnn02np1  16396  sumeven  16435  ncoprmgcdne1b  16698  dvdsprmpweqnn  16935  prmodvdslcmf  17097  sgrpass  18773  symgextf1  19482  fvcosymgeq  19490  ricgic  20581  zringndrg  21578  evlslem4  22187  scmatf1  22649  pmatcoe1fsupp  22819  t1sncld  23444  regsep  23452  nrmsep3  23473  cmpsublem  23517  ufilss  24023  fclscf  24143  ncvsprp  25272  ncvsm1  25274  ncvsdif  25275  ncvspi  25276  ncvspds  25281  mblsplit  25652  mbfdm  25746  fta1glem1  26286  aaliou2  26462  dvloglem  26771  lgsqrlem4  27471  2sqnn0  27560  ausgrusgrb  29424  fusgredgfi  29584  vtxdumgrval  29745  vtxdginducedm1lem4  29801  umgrn1cycl  30065  hashecclwwlkn1  30337  umgrhashecclwwlk  30338  0spth  30386  eucrctshift  30503  frcond1  30526  2pthfrgr  30544  frgrncvvdeqlem7  30565  frgrncvvdeq  30569  frgrwopreglem3  30574  frgrwopreglem5lem  30580  frgr2wwlk1  30589  numclwwlk1lem2f1  30617  hhcms  31464  stcltr1i  32535  chpssati  32624  bnj570  35210  bnj1145  35298  bnj1398  35339  bnj1442  35354  sconnpht  35592  fmla1  35750  goalrlem  35759  goalr  35760  satfv0fvfmla0  35776  fununiq  36132  rdgprc0  36154  bj-substw  37212  bj-opelresdm  37649  poimirlem25  38156  funressnfv  47635  funressnvmo  47637  euoreqb  47701  fcdmvafv2v  47828  dfatbrafv2b  47837  prproropf1olem4  48110  lighneallem2  48213  grlimgrtrilem2  48622  pgnioedg1  48728  pgnioedg2  48729  pgnioedg3  48730  pgnioedg4  48731  pgnioedg5  48732  pgnbgreunbgrlem2lem1  48734  pgnbgreunbgrlem2lem2  48735  pgnbgreunbgrlem2lem3  48736  pgnbgreunbgrlem5lem1  48740  pgnbgreunbgrlem5lem2  48741  pgnbgreunbgrlem5lem3  48742  lindslinindsimp1  49088  fullthinc  50079