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  3872  dfss2  3944  solin  5588  xpidtr  6111  funimaexgOLD  6624  f1ssres  6781  fvn0ssdmfun  7064  f1veqaeq  7249  f1opw  7663  resf1extb  7930  fprlem1  8299  ixpn0  8944  domunsncan  9086  phplem2  9219  php3  9223  php3OLD  9233  infsupprpr  9518  frrlem15  9771  dfac9  10151  ltxrlt  11305  znegcl  12627  zltaddlt1le  13522  injresinj  13804  fsuppmapnn0fiubex  14010  pfxccatin12lem3  14750  repswswrd  14802  oddnn02np1  16367  sumeven  16406  ncoprmgcdne1b  16669  dvdsprmpweqnn  16905  prmodvdslcmf  17067  sgrpass  18703  symgextf1  19402  fvcosymgeq  19410  ricgic  20467  zringndrg  21429  evlslem4  22034  scmatf1  22469  pmatcoe1fsupp  22639  t1sncld  23264  regsep  23272  nrmsep3  23293  cmpsublem  23337  ufilss  23843  fclscf  23963  ncvsprp  25104  ncvsm1  25106  ncvsdif  25107  ncvspi  25108  ncvspds  25113  mblsplit  25485  mbfdm  25579  fta1glem1  26125  aaliou2  26300  dvloglem  26609  lgsqrlem4  27312  2sqnn0  27401  ausgrusgrb  29144  fusgredgfi  29304  vtxdumgrval  29466  vtxdginducedm1lem4  29522  umgrn1cycl  29789  hashecclwwlkn1  30058  umgrhashecclwwlk  30059  0spth  30107  eucrctshift  30224  frcond1  30247  2pthfrgr  30265  frgrncvvdeqlem7  30286  frgrncvvdeq  30290  frgrwopreglem3  30295  frgrwopreglem5lem  30301  frgr2wwlk1  30310  numclwwlk1lem2f1  30338  hhcms  31184  stcltr1i  32255  bnj570  34936  bnj1145  35024  bnj1398  35065  bnj1442  35080  sconnpht  35251  fmla1  35409  goalrlem  35418  goalr  35419  satfv0fvfmla0  35435  fununiq  35786  rdgprc0  35811  bj-substw  36740  bj-opelresdm  37163  poimirlem25  37669  funressnfv  47072  funressnvmo  47074  euoreqb  47138  fcdmvafv2v  47265  dfatbrafv2b  47274  prproropf1olem4  47520  lighneallem2  47620  grlimgrtrilem2  48007  lindslinindsimp1  48433  fullthinc  49336