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  3835  dfss2  3907  solin  5566  xpidtr  6085  f1ssres  6743  fvn0ssdmfun  7026  f1veqaeq  7211  f1opw  7623  resf1extb  7885  fprlem1  8250  ixpn0  8878  domunsncan  9015  phplem2  9139  php3  9143  infsupprpr  9419  frrlem15  9681  dfac9  10059  ltxrlt  11216  znegcl  12562  zltaddlt1le  13458  injresinj  13746  fsuppmapnn0fiubex  13954  pfxccatin12lem3  14694  repswswrd  14746  oddnn02np1  16317  sumeven  16356  ncoprmgcdne1b  16619  dvdsprmpweqnn  16856  prmodvdslcmf  17018  sgrpass  18693  symgextf1  19396  fvcosymgeq  19404  ricgic  20484  zringndrg  21448  evlslem4  22054  scmatf1  22496  pmatcoe1fsupp  22666  t1sncld  23291  regsep  23299  nrmsep3  23320  cmpsublem  23364  ufilss  23870  fclscf  23990  ncvsprp  25119  ncvsm1  25121  ncvsdif  25122  ncvspi  25123  ncvspds  25128  mblsplit  25499  mbfdm  25593  fta1glem1  26133  aaliou2  26306  dvloglem  26612  lgsqrlem4  27312  2sqnn0  27401  ausgrusgrb  29234  fusgredgfi  29394  vtxdumgrval  29555  vtxdginducedm1lem4  29611  umgrn1cycl  29875  hashecclwwlkn1  30147  umgrhashecclwwlk  30148  0spth  30196  eucrctshift  30313  frcond1  30336  2pthfrgr  30354  frgrncvvdeqlem7  30375  frgrncvvdeq  30379  frgrwopreglem3  30384  frgrwopreglem5lem  30390  frgr2wwlk1  30399  numclwwlk1lem2f1  30427  hhcms  31274  stcltr1i  32345  chpssati  32434  bnj570  35047  bnj1145  35135  bnj1398  35176  bnj1442  35191  sconnpht  35411  fmla1  35569  goalrlem  35578  goalr  35579  satfv0fvfmla0  35595  fununiq  35951  rdgprc0  35973  bj-substw  37022  bj-opelresdm  37459  poimirlem25  37966  funressnfv  47491  funressnvmo  47493  euoreqb  47557  fcdmvafv2v  47684  dfatbrafv2b  47693  prproropf1olem4  47966  lighneallem2  48069  grlimgrtrilem2  48478  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  lindslinindsimp1  48933  fullthinc  49925