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  3847  dfss2  3919  solin  5559  xpidtr  6079  f1ssres  6737  fvn0ssdmfun  7019  f1veqaeq  7202  f1opw  7614  resf1extb  7876  fprlem1  8242  ixpn0  8868  domunsncan  9005  phplem2  9129  php3  9133  infsupprpr  9409  frrlem15  9669  dfac9  10047  ltxrlt  11203  znegcl  12526  zltaddlt1le  13421  injresinj  13707  fsuppmapnn0fiubex  13915  pfxccatin12lem3  14655  repswswrd  14707  oddnn02np1  16275  sumeven  16314  ncoprmgcdne1b  16577  dvdsprmpweqnn  16813  prmodvdslcmf  16975  sgrpass  18650  symgextf1  19350  fvcosymgeq  19358  ricgic  20440  zringndrg  21423  evlslem4  22031  scmatf1  22475  pmatcoe1fsupp  22645  t1sncld  23270  regsep  23278  nrmsep3  23299  cmpsublem  23343  ufilss  23849  fclscf  23969  ncvsprp  25108  ncvsm1  25110  ncvsdif  25111  ncvspi  25112  ncvspds  25117  mblsplit  25489  mbfdm  25583  fta1glem1  26129  aaliou2  26304  dvloglem  26613  lgsqrlem4  27316  2sqnn0  27405  ausgrusgrb  29238  fusgredgfi  29398  vtxdumgrval  29560  vtxdginducedm1lem4  29616  umgrn1cycl  29880  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  0spth  30201  eucrctshift  30318  frcond1  30341  2pthfrgr  30359  frgrncvvdeqlem7  30380  frgrncvvdeq  30384  frgrwopreglem3  30389  frgrwopreglem5lem  30395  frgr2wwlk1  30404  numclwwlk1lem2f1  30432  hhcms  31278  stcltr1i  32349  chpssati  32438  bnj570  35061  bnj1145  35149  bnj1398  35190  bnj1442  35205  sconnpht  35423  fmla1  35581  goalrlem  35590  goalr  35591  satfv0fvfmla0  35607  fununiq  35963  rdgprc0  35985  bj-substw  36923  bj-opelresdm  37346  poimirlem25  37842  funressnfv  47285  funressnvmo  47287  euoreqb  47351  fcdmvafv2v  47478  dfatbrafv2b  47487  prproropf1olem4  47748  lighneallem2  47848  grlimgrtrilem2  48244  pgnioedg1  48350  pgnioedg2  48351  pgnioedg3  48352  pgnioedg4  48353  pgnioedg5  48354  pgnbgreunbgrlem2lem1  48356  pgnbgreunbgrlem2lem2  48357  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem5lem1  48362  pgnbgreunbgrlem5lem2  48363  pgnbgreunbgrlem5lem3  48364  lindslinindsimp1  48699  fullthinc  49691