Theorem simplbiim 514

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  2reu1  3845  dfss2  3917  solin  5586  xpidtr  6114  f1ssres  6779  fvn0ssdmfun  7066  f1veqaeq  7252  f1opw  7669  resf1extb  7935  fprlem1  8302  ixpn0  8942  domunsncan  9080  phplem2  9204  php3  9208  infsupprpr  9482  frrlem15  9745  dfac9  10196  ltxrlt  11361  znegcl  12712  zltaddlt1le  13617  injresinj  13906  fsuppmapnn0fiubex  14115  pfxccatin12lem3  14861  repswswrd  14915  oddnn02np1  16498  sumeven  16537  ncoprmgcdne1b  16805  dvdsprmpweqnn  17043  prmodvdslcmf  17205  sgrpass  18894  symgextf1  19615  fvcosymgeq  19623  ricgic  20735  zringndrg  21754  evlslem4  22365  scmatf1  22826  pmatcoe1fsupp  22999  t1sncld  23624  regsep  23632  nrmsep3  23653  cmpsublem  23697  ufilss  24204  fclscf  24324  ncvsprp  25453  ncvsm1  25455  ncvsdif  25456  ncvspi  25457  ncvspds  25462  mblsplit  25833  mbfdm  25927  fta1glem1  26466  aaliou2  26649  dvloglem  26958  lgsqrlem4  27658  2sqnn0  27747  ausgrusgrb  29728  fusgredgfi  29888  vtxdumgrval  30049  vtxdginducedm1lem4  30105  umgrn1cycl  30378  hashecclwwlkn1  30650  umgrhashecclwwlk  30651  0spth  30699  eucrctshift  30826  frcond1  30849  2pthfrgr  30867  frgrncvvdeqlem7  30888  frgrncvvdeq  30892  frgrwopreglem3  30897  frgrwopreglem5lem  30903  frgr2wwlk1  30912  numclwwlk1lem2f1  30940  hhcms  31787  stcltr1i  32858  chpssati  32947  bnj570  35518  bnj1145  35606  bnj1398  35647  bnj1442  35662  sconnpht  35963  fmla1  36121  goalrlem  36130  goalr  36131  satfv0fvfmla0  36147  fununiq  36503  rdgprc0  36525  bj-substw  37597  bj-opelresdm  38034  poimirlem25  38531  funressnfv  48057  funressnvmo  48059  euoreqb  48123  fcdmvafv2v  48250  dfatbrafv2b  48259  prproropf1olem4  48532  lighneallem2  48635  grlimgrtrilem2  49044  pgnioedg1  49150  pgnioedg2  49151  pgnioedg3  49152  pgnioedg4  49153  pgnioedg5  49154  pgnbgreunbgrlem2lem1  49156  pgnbgreunbgrlem2lem2  49157  pgnbgreunbgrlem2lem3  49158  pgnbgreunbgrlem5lem1  49162  pgnbgreunbgrlem5lem2  49163  pgnbgreunbgrlem5lem3  49164  lindslinindsimp1  49513  fullthinc  50502