Theorem simplbiim 512

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  2reu1  3850  dfss2  3922  solin  5580  xpidtr  6106  f1ssres  6765  fvn0ssdmfun  7051  f1veqaeq  7236  f1opw  7648  resf1extb  7911  fprlem1  8276  ixpn0  8908  domunsncan  9045  phplem2  9169  php3  9173  infsupprpr  9449  frrlem15  9712  dfac9  10090  ltxrlt  11250  znegcl  12603  zltaddlt1le  13506  injresinj  13794  fsuppmapnn0fiubex  14002  pfxccatin12lem3  14742  repswswrd  14794  oddnn02np1  16365  sumeven  16404  ncoprmgcdne1b  16667  dvdsprmpweqnn  16904  prmodvdslcmf  17066  sgrpass  18742  symgextf1  19444  fvcosymgeq  19452  ricgic  20536  zringndrg  21500  evlslem4  22109  scmatf1  22571  pmatcoe1fsupp  22741  t1sncld  23366  regsep  23374  nrmsep3  23395  cmpsublem  23439  ufilss  23945  fclscf  24065  ncvsprp  25194  ncvsm1  25196  ncvsdif  25197  ncvspi  25198  ncvspds  25203  mblsplit  25574  mbfdm  25668  fta1glem1  26208  aaliou2  26381  dvloglem  26690  lgsqrlem4  27390  2sqnn0  27479  ausgrusgrb  29312  fusgredgfi  29472  vtxdumgrval  29633  vtxdginducedm1lem4  29689  umgrn1cycl  29953  hashecclwwlkn1  30225  umgrhashecclwwlk  30226  0spth  30274  eucrctshift  30391  frcond1  30414  2pthfrgr  30432  frgrncvvdeqlem7  30453  frgrncvvdeq  30457  frgrwopreglem3  30462  frgrwopreglem5lem  30468  frgr2wwlk1  30477  numclwwlk1lem2f1  30505  hhcms  31352  stcltr1i  32423  chpssati  32512  bnj570  35164  bnj1145  35252  bnj1398  35293  bnj1442  35308  sconnpht  35543  fmla1  35701  goalrlem  35710  goalr  35711  satfv0fvfmla0  35727  fununiq  36083  rdgprc0  36105  bj-substw  37164  bj-opelresdm  37601  poimirlem25  38108  funressnfv  47601  funressnvmo  47603  euoreqb  47667  fcdmvafv2v  47794  dfatbrafv2b  47803  prproropf1olem4  48076  lighneallem2  48179  grlimgrtrilem2  48588  pgnioedg1  48694  pgnioedg2  48695  pgnioedg3  48696  pgnioedg4  48697  pgnioedg5  48698  pgnbgreunbgrlem2lem1  48700  pgnbgreunbgrlem2lem2  48701  pgnbgreunbgrlem2lem3  48702  pgnbgreunbgrlem5lem1  48706  pgnbgreunbgrlem5lem2  48707  pgnbgreunbgrlem5lem3  48708  lindslinindsimp1  49043  fullthinc  50035