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  3859  dfss2  3931  solin  5597  xpidtr  6123  f1ssres  6784  fvn0ssdmfun  7070  f1veqaeq  7255  f1opw  7667  resf1extb  7931  fprlem1  8297  ixpn0  8928  domunsncan  9065  phplem2  9189  php3  9193  infsupprpr  9466  frrlem15  9729  dfac9  10120  ltxrlt  11280  znegcl  12629  zltaddlt1le  13532  injresinj  13820  fsuppmapnn0fiubex  14028  pfxccatin12lem3  14769  repswswrd  14821  oddnn02np1  16406  sumeven  16445  ncoprmgcdne1b  16708  dvdsprmpweqnn  16945  prmodvdslcmf  17107  sgrpass  18783  symgextf1  19491  fvcosymgeq  19499  ricgic  20590  zringndrg  21587  evlslem4  22196  scmatf1  22657  pmatcoe1fsupp  22827  t1sncld  23452  regsep  23460  nrmsep3  23481  cmpsublem  23525  ufilss  24031  fclscf  24151  ncvsprp  25280  ncvsm1  25282  ncvsdif  25283  ncvspi  25284  ncvspds  25289  mblsplit  25660  mbfdm  25754  fta1glem1  26294  aaliou2  26470  dvloglem  26779  lgsqrlem4  27479  2sqnn0  27568  ausgrusgrb  29456  fusgredgfi  29616  vtxdumgrval  29777  vtxdginducedm1lem4  29833  umgrn1cycl  30097  hashecclwwlkn1  30369  umgrhashecclwwlk  30370  0spth  30418  eucrctshift  30535  frcond1  30558  2pthfrgr  30576  frgrncvvdeqlem7  30597  frgrncvvdeq  30601  frgrwopreglem3  30606  frgrwopreglem5lem  30612  frgr2wwlk1  30621  numclwwlk1lem2f1  30649  hhcms  31496  stcltr1i  32567  chpssati  32656  bnj570  35238  bnj1145  35326  bnj1398  35367  bnj1442  35382  sconnpht  35654  fmla1  35812  goalrlem  35821  goalr  35822  satfv0fvfmla0  35838  fununiq  36194  rdgprc0  36216  bj-substw  37273  bj-opelresdm  37711  poimirlem25  38218  funressnfv  47703  funressnvmo  47705  euoreqb  47769  fcdmvafv2v  47896  dfatbrafv2b  47905  prproropf1olem4  48178  lighneallem2  48281  grlimgrtrilem2  48690  pgnioedg1  48796  pgnioedg2  48797  pgnioedg3  48798  pgnioedg4  48799  pgnioedg5  48800  pgnbgreunbgrlem2lem1  48802  pgnbgreunbgrlem2lem2  48803  pgnbgreunbgrlem2lem3  48804  pgnbgreunbgrlem5lem1  48808  pgnbgreunbgrlem5lem2  48809  pgnbgreunbgrlem5lem3  48810  lindslinindsimp1  49156  fullthinc  50147