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  3852  dfss2  3924  solin  5598  xpidtr  6124  f1ssres  6785  fvn0ssdmfun  7071  f1veqaeq  7256  f1opw  7668  resf1extb  7932  fprlem1  8298  ixpn0  8929  domunsncan  9066  phplem2  9190  php3  9194  infsupprpr  9467  frrlem15  9730  dfac9  10121  ltxrlt  11281  znegcl  12630  zltaddlt1le  13533  injresinj  13822  fsuppmapnn0fiubex  14030  pfxccatin12lem3  14771  repswswrd  14823  oddnn02np1  16407  sumeven  16446  ncoprmgcdne1b  16709  dvdsprmpweqnn  16946  prmodvdslcmf  17108  sgrpass  18784  symgextf1  19492  fvcosymgeq  19500  ricgic  20591  zringndrg  21599  evlslem4  22208  scmatf1  22669  pmatcoe1fsupp  22839  t1sncld  23464  regsep  23472  nrmsep3  23493  cmpsublem  23537  ufilss  24043  fclscf  24163  ncvsprp  25292  ncvsm1  25294  ncvsdif  25295  ncvspi  25296  ncvspds  25301  mblsplit  25672  mbfdm  25766  fta1glem1  26306  aaliou2  26482  dvloglem  26791  lgsqrlem4  27491  2sqnn0  27580  ausgrusgrb  29493  fusgredgfi  29653  vtxdumgrval  29814  vtxdginducedm1lem4  29870  umgrn1cycl  30134  hashecclwwlkn1  30406  umgrhashecclwwlk  30407  0spth  30455  eucrctshift  30572  frcond1  30595  2pthfrgr  30613  frgrncvvdeqlem7  30634  frgrncvvdeq  30638  frgrwopreglem3  30643  frgrwopreglem5lem  30649  frgr2wwlk1  30658  numclwwlk1lem2f1  30686  hhcms  31533  stcltr1i  32604  chpssati  32693  bnj570  35271  bnj1145  35359  bnj1398  35400  bnj1442  35415  sconnpht  35699  fmla1  35857  goalrlem  35866  goalr  35867  satfv0fvfmla0  35883  fununiq  36239  rdgprc0  36261  bj-substw  37328  bj-opelresdm  37767  poimirlem25  38274  funressnfv  47757  funressnvmo  47759  euoreqb  47823  fcdmvafv2v  47950  dfatbrafv2b  47959  prproropf1olem4  48232  lighneallem2  48335  grlimgrtrilem2  48744  pgnioedg1  48850  pgnioedg2  48851  pgnioedg3  48852  pgnioedg4  48853  pgnioedg5  48854  pgnbgreunbgrlem2lem1  48856  pgnbgreunbgrlem2lem2  48857  pgnbgreunbgrlem2lem3  48858  pgnbgreunbgrlem5lem1  48862  pgnbgreunbgrlem5lem2  48863  pgnbgreunbgrlem5lem3  48864  lindslinindsimp1  49214  fullthinc  50205