Theorem simplbiim 506

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 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  2reu1  3892  invdisjrab  5135  solin  5614  xpidtr  6124  funimaexgOLD  6636  f1ssres  6796  fvn0ssdmfun  7077  f1veqaeq  7256  f1opw  7662  fprlem1  8285  ixpn0  8924  domunsncan  9072  phplem2  9208  php3  9212  phplem4OLD  9220  php3OLD  9224  infsupprpr  9499  frrlem15  9752  dfac9  10131  ltxrlt  11284  znegcl  12597  zltaddlt1le  13482  injresinj  13753  fsuppmapnn0fiubex  13957  pfxccatin12lem3  14682  repswswrd  14734  oddnn02np1  16291  sumeven  16330  ncoprmgcdne1b  16587  dvdsprmpweqnn  16818  prmodvdslcmf  16980  sgrpass  18616  symgextf1  19289  fvcosymgeq  19297  ricgic  20286  zringndrg  21038  evlslem4  21637  scmatf1  22033  pmatcoe1fsupp  22203  t1sncld  22830  regsep  22838  nrmsep3  22859  cmpsublem  22903  ufilss  23409  fclscf  23529  ncvsprp  24669  ncvsm1  24671  ncvsdif  24672  ncvspi  24673  ncvspds  24678  mblsplit  25049  mbfdm  25143  fta1glem1  25683  aaliou2  25853  dvloglem  26156  lgsqrlem4  26852  2sqnn0  26941  ausgrusgrb  28425  fusgredgfi  28582  vtxdumgrval  28743  vtxdginducedm1lem4  28799  umgrn1cycl  29061  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  0spth  29379  eucrctshift  29496  frcond1  29519  2pthfrgr  29537  frgrncvvdeqlem7  29558  frgrncvvdeq  29562  frgrwopreglem3  29567  frgrwopreglem5lem  29573  frgr2wwlk1  29582  numclwwlk1lem2f1  29610  hhcms  30456  stcltr1i  31527  bnj570  33916  bnj1145  34004  bnj1398  34045  bnj1442  34060  sconnpht  34220  fmla1  34378  goalrlem  34387  goalr  34388  satfv0fvfmla0  34404  fununiq  34740  rdgprc0  34765  bj-substw  35600  bj-opelresdm  36026  poimirlem25  36513  funressnfv  45753  funressnvmo  45755  euoreqb  45817  fcdmvafv2v  45944  dfatbrafv2b  45953  prproropf1olem4  46174  lighneallem2  46274  lindslinindsimp1  47138  fullthinc  47666