Theorem simplbiim 504

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  2reu1  3836  dfss2  3908  solin  5559  xpidtr  6079  f1ssres  6737  fvn0ssdmfun  7020  f1veqaeq  7204  f1opw  7616  resf1extb  7878  fprlem1  8243  ixpn0  8871  domunsncan  9008  phplem2  9132  php3  9136  infsupprpr  9412  frrlem15  9672  dfac9  10050  ltxrlt  11207  znegcl  12553  zltaddlt1le  13449  injresinj  13737  fsuppmapnn0fiubex  13945  pfxccatin12lem3  14685  repswswrd  14737  oddnn02np1  16308  sumeven  16347  ncoprmgcdne1b  16610  dvdsprmpweqnn  16847  prmodvdslcmf  17009  sgrpass  18684  symgextf1  19387  fvcosymgeq  19395  ricgic  20475  zringndrg  21458  evlslem4  22064  scmatf1  22506  pmatcoe1fsupp  22676  t1sncld  23301  regsep  23309  nrmsep3  23330  cmpsublem  23374  ufilss  23880  fclscf  24000  ncvsprp  25129  ncvsm1  25131  ncvsdif  25132  ncvspi  25133  ncvspds  25138  mblsplit  25509  mbfdm  25603  fta1glem1  26143  aaliou2  26317  dvloglem  26625  lgsqrlem4  27326  2sqnn0  27415  ausgrusgrb  29248  fusgredgfi  29408  vtxdumgrval  29570  vtxdginducedm1lem4  29626  umgrn1cycl  29890  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  0spth  30211  eucrctshift  30328  frcond1  30351  2pthfrgr  30369  frgrncvvdeqlem7  30390  frgrncvvdeq  30394  frgrwopreglem3  30399  frgrwopreglem5lem  30405  frgr2wwlk1  30414  numclwwlk1lem2f1  30442  hhcms  31289  stcltr1i  32360  chpssati  32449  bnj570  35063  bnj1145  35151  bnj1398  35192  bnj1442  35207  sconnpht  35427  fmla1  35585  goalrlem  35594  goalr  35595  satfv0fvfmla0  35611  fununiq  35967  rdgprc0  35989  bj-substw  37038  bj-opelresdm  37475  poimirlem25  37980  funressnfv  47503  funressnvmo  47505  euoreqb  47569  fcdmvafv2v  47696  dfatbrafv2b  47705  prproropf1olem4  47978  lighneallem2  48081  grlimgrtrilem2  48490  pgnioedg1  48596  pgnioedg2  48597  pgnioedg3  48598  pgnioedg4  48599  pgnioedg5  48600  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5lem3  48610  lindslinindsimp1  48945  fullthinc  49937