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 496	. 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  3860  dfss2  3932  solin  5573  xpidtr  6095  funimaexgOLD  6604  f1ssres  6763  fvn0ssdmfun  7046  f1veqaeq  7231  f1opw  7645  resf1extb  7910  fprlem1  8279  ixpn0  8903  domunsncan  9041  phplem2  9169  php3  9173  infsupprpr  9457  frrlem15  9710  dfac9  10090  ltxrlt  11244  znegcl  12568  zltaddlt1le  13466  injresinj  13749  fsuppmapnn0fiubex  13957  pfxccatin12lem3  14697  repswswrd  14749  oddnn02np1  16318  sumeven  16357  ncoprmgcdne1b  16620  dvdsprmpweqnn  16856  prmodvdslcmf  17018  sgrpass  18652  symgextf1  19351  fvcosymgeq  19359  ricgic  20416  zringndrg  21378  evlslem4  21983  scmatf1  22418  pmatcoe1fsupp  22588  t1sncld  23213  regsep  23221  nrmsep3  23242  cmpsublem  23286  ufilss  23792  fclscf  23912  ncvsprp  25052  ncvsm1  25054  ncvsdif  25055  ncvspi  25056  ncvspds  25061  mblsplit  25433  mbfdm  25527  fta1glem1  26073  aaliou2  26248  dvloglem  26557  lgsqrlem4  27260  2sqnn0  27349  ausgrusgrb  29092  fusgredgfi  29252  vtxdumgrval  29414  vtxdginducedm1lem4  29470  umgrn1cycl  29737  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  0spth  30055  eucrctshift  30172  frcond1  30195  2pthfrgr  30213  frgrncvvdeqlem7  30234  frgrncvvdeq  30238  frgrwopreglem3  30243  frgrwopreglem5lem  30249  frgr2wwlk1  30258  numclwwlk1lem2f1  30286  hhcms  31132  stcltr1i  32203  bnj570  34895  bnj1145  34983  bnj1398  35024  bnj1442  35039  sconnpht  35216  fmla1  35374  goalrlem  35383  goalr  35384  satfv0fvfmla0  35400  fununiq  35756  rdgprc0  35781  bj-substw  36710  bj-opelresdm  37133  poimirlem25  37639  funressnfv  47044  funressnvmo  47046  euoreqb  47110  fcdmvafv2v  47237  dfatbrafv2b  47246  prproropf1olem4  47507  lighneallem2  47607  grlimgrtrilem2  47994  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  lindslinindsimp1  48446  fullthinc  49439