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  3849  dfss2  3921  solin  5567  xpidtr  6087  f1ssres  6745  fvn0ssdmfun  7028  f1veqaeq  7212  f1opw  7624  resf1extb  7886  fprlem1  8252  ixpn0  8880  domunsncan  9017  phplem2  9141  php3  9145  infsupprpr  9421  frrlem15  9681  dfac9  10059  ltxrlt  11215  znegcl  12538  zltaddlt1le  13433  injresinj  13719  fsuppmapnn0fiubex  13927  pfxccatin12lem3  14667  repswswrd  14719  oddnn02np1  16287  sumeven  16326  ncoprmgcdne1b  16589  dvdsprmpweqnn  16825  prmodvdslcmf  16987  sgrpass  18662  symgextf1  19362  fvcosymgeq  19370  ricgic  20452  zringndrg  21435  evlslem4  22043  scmatf1  22487  pmatcoe1fsupp  22657  t1sncld  23282  regsep  23290  nrmsep3  23311  cmpsublem  23355  ufilss  23861  fclscf  23981  ncvsprp  25120  ncvsm1  25122  ncvsdif  25123  ncvspi  25124  ncvspds  25129  mblsplit  25501  mbfdm  25595  fta1glem1  26141  aaliou2  26316  dvloglem  26625  lgsqrlem4  27328  2sqnn0  27417  ausgrusgrb  29250  fusgredgfi  29410  vtxdumgrval  29572  vtxdginducedm1lem4  29628  umgrn1cycl  29892  hashecclwwlkn1  30164  umgrhashecclwwlk  30165  0spth  30213  eucrctshift  30330  frcond1  30353  2pthfrgr  30371  frgrncvvdeqlem7  30392  frgrncvvdeq  30396  frgrwopreglem3  30401  frgrwopreglem5lem  30407  frgr2wwlk1  30416  numclwwlk1lem2f1  30444  hhcms  31290  stcltr1i  32361  chpssati  32450  bnj570  35080  bnj1145  35168  bnj1398  35209  bnj1442  35224  sconnpht  35442  fmla1  35600  goalrlem  35609  goalr  35610  satfv0fvfmla0  35626  fununiq  35982  rdgprc0  36004  bj-substw  36962  bj-opelresdm  37394  poimirlem25  37890  funressnfv  47397  funressnvmo  47399  euoreqb  47463  fcdmvafv2v  47590  dfatbrafv2b  47599  prproropf1olem4  47860  lighneallem2  47960  grlimgrtrilem2  48356  pgnioedg1  48462  pgnioedg2  48463  pgnioedg3  48464  pgnioedg4  48465  pgnioedg5  48466  pgnbgreunbgrlem2lem1  48468  pgnbgreunbgrlem2lem2  48469  pgnbgreunbgrlem2lem3  48470  pgnbgreunbgrlem5lem1  48474  pgnbgreunbgrlem5lem2  48475  pgnbgreunbgrlem5lem3  48476  lindslinindsimp1  48811  fullthinc  49803