Theorem simplbiim 514

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  2reu1  3844  dfss2  4094  solin  5585  xpidtr  6115  fununiq  6555  f1ssres  6787  fvn0ssdmfun  7074  f1veqaeq  7260  f1opw  7677  resf1extb  7946  fprlem1  8321  ixpn0  8961  domunsncan  9099  phplem2  9223  php3  9227  infsupprpr  9501  frrlem15  9764  dfac9  10218  ltxrlt  11383  znegcl  12734  zltaddlt1le  13639  injresinj  13929  fsuppmapnn0fiubex  14138  pfxccatin12lem3  14885  repswswrd  14939  oddnn02np1  16523  sumeven  16562  ncoprmgcdne1b  16830  dvdsprmpweqnn  17068  prmodvdslcmf  17230  sgrpass  18919  symgextf1  19640  fvcosymgeq  19648  ricgic  20760  zringndrg  21779  evlslem4  22390  scmatf1  22851  pmatcoe1fsupp  23024  t1sncld  23649  regsep  23657  nrmsep3  23678  cmpsublem  23722  ufilss  24229  fclscf  24349  ncvsprp  25478  ncvsm1  25480  ncvsdif  25481  ncvspi  25482  ncvspds  25487  mblsplit  25858  mbfdm  25952  fta1glem1  26491  aaliou2  26672  dvloglem  26981  lgsqrlem4  27681  2sqnn0  27770  ausgrusgrb  29751  fusgredgfi  29911  vtxdumgrval  30072  vtxdginducedm1lem4  30128  umgrn1cycl  30401  hashecclwwlkn1  30673  umgrhashecclwwlk  30674  0spth  30722  eucrctshift  30849  frcond1  30872  2pthfrgr  30890  frgrncvvdeqlem7  30911  frgrncvvdeq  30915  frgrwopreglem3  30920  frgrwopreglem5lem  30926  frgr2wwlk1  30935  numclwwlk1lem2f1  30963  hhcms  31810  stcltr1i  32881  chpssati  32970  bnj570  35581  bnj1145  35669  bnj1398  35710  bnj1442  35725  sconnpht  36080  fmla1  36238  goalrlem  36247  goalr  36248  satfv0fvfmla0  36264  rdgprc0  36647  bj-substw  37719  bj-opelresdm  38159  poimirlem25  38656  funressnfv  48206  funressnvmo  48208  euoreqb  48272  fcdmvafv2v  48399  dfatbrafv2b  48408  prproropf1olem4  48681  lighneallem2  48784  grlimgrtrilem2  49193  pgnioedg1  49299  pgnioedg2  49300  pgnioedg3  49301  pgnioedg4  49302  pgnioedg5  49303  pgnbgreunbgrlem2lem1  49305  pgnbgreunbgrlem2lem2  49306  pgnbgreunbgrlem2lem3  49307  pgnbgreunbgrlem5lem1  49311  pgnbgreunbgrlem5lem2  49312  pgnbgreunbgrlem5lem3  49313  lindslinindsimp1  49662  fullthinc  50678