Theorem simplbiim 509

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  2reu1  3836  dfss2  3908  solin  5560  xpidtr  6079  f1ssres  6737  fvn0ssdmfun  7022  f1veqaeq  7207  f1opw  7619  resf1extb  7881  fprlem1  8247  ixpn0  8875  domunsncan  9012  phplem2  9136  php3  9140  infsupprpr  9416  frrlem15  9679  dfac9  10057  ltxrlt  11214  znegcl  12560  zltaddlt1le  13456  injresinj  13744  fsuppmapnn0fiubex  13952  pfxccatin12lem3  14692  repswswrd  14744  oddnn02np1  16315  sumeven  16354  ncoprmgcdne1b  16617  dvdsprmpweqnn  16854  prmodvdslcmf  17016  sgrpass  18691  symgextf1  19394  fvcosymgeq  19402  ricgic  20486  zringndrg  21450  evlslem4  22059  scmatf1  22521  pmatcoe1fsupp  22691  t1sncld  23316  regsep  23324  nrmsep3  23345  cmpsublem  23389  ufilss  23895  fclscf  24015  ncvsprp  25144  ncvsm1  25146  ncvsdif  25147  ncvspi  25148  ncvspds  25153  mblsplit  25524  mbfdm  25618  fta1glem1  26158  aaliou2  26331  dvloglem  26637  lgsqrlem4  27337  2sqnn0  27426  ausgrusgrb  29259  fusgredgfi  29419  vtxdumgrval  29580  vtxdginducedm1lem4  29636  umgrn1cycl  29900  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  0spth  30221  eucrctshift  30338  frcond1  30361  2pthfrgr  30379  frgrncvvdeqlem7  30400  frgrncvvdeq  30404  frgrwopreglem3  30409  frgrwopreglem5lem  30415  frgr2wwlk1  30424  numclwwlk1lem2f1  30452  hhcms  31299  stcltr1i  32370  chpssati  32459  bnj570  35094  bnj1145  35182  bnj1398  35223  bnj1442  35238  sconnpht  35464  fmla1  35622  goalrlem  35631  goalr  35632  satfv0fvfmla0  35648  fununiq  36004  rdgprc0  36026  bj-substw  37075  bj-opelresdm  37512  poimirlem25  38019  funressnfv  47513  funressnvmo  47515  euoreqb  47579  fcdmvafv2v  47706  dfatbrafv2b  47715  prproropf1olem4  47988  lighneallem2  48091  grlimgrtrilem2  48500  pgnioedg1  48606  pgnioedg2  48607  pgnioedg3  48608  pgnioedg4  48609  pgnioedg5  48610  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem5lem1  48618  pgnbgreunbgrlem5lem2  48619  pgnbgreunbgrlem5lem3  48620  lindslinindsimp1  48955  fullthinc  49947