Theorem simplbiim 503

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 395

This theorem is referenced by:  2reu1  3889  dfss2  3964  invdisjrab  5131  solin  5611  xpidtr  6126  funimaexgOLD  6638  f1ssres  6797  fvn0ssdmfun  7080  f1veqaeq  7264  f1opw  7674  fprlem1  8307  ixpn0  8951  domunsncan  9102  phplem2  9235  php3  9239  phplem4OLD  9247  php3OLD  9251  infsupprpr  9540  frrlem15  9793  dfac9  10172  ltxrlt  11325  znegcl  12643  zltaddlt1le  13530  injresinj  13802  fsuppmapnn0fiubex  14006  pfxccatin12lem3  14735  repswswrd  14787  oddnn02np1  16345  sumeven  16384  ncoprmgcdne1b  16646  dvdsprmpweqnn  16882  prmodvdslcmf  17044  sgrpass  18713  symgextf1  19415  fvcosymgeq  19423  ricgic  20485  zringndrg  21454  evlslem4  22085  scmatf1  22521  pmatcoe1fsupp  22691  t1sncld  23318  regsep  23326  nrmsep3  23347  cmpsublem  23391  ufilss  23897  fclscf  24017  ncvsprp  25168  ncvsm1  25170  ncvsdif  25171  ncvspi  25172  ncvspds  25177  mblsplit  25549  mbfdm  25643  fta1glem1  26192  aaliou2  26365  dvloglem  26672  lgsqrlem4  27375  2sqnn0  27464  ausgrusgrb  29098  fusgredgfi  29258  vtxdumgrval  29420  vtxdginducedm1lem4  29476  umgrn1cycl  29738  hashecclwwlkn1  30007  umgrhashecclwwlk  30008  0spth  30056  eucrctshift  30173  frcond1  30196  2pthfrgr  30214  frgrncvvdeqlem7  30235  frgrncvvdeq  30239  frgrwopreglem3  30244  frgrwopreglem5lem  30250  frgr2wwlk1  30259  numclwwlk1lem2f1  30287  hhcms  31133  stcltr1i  32204  bnj570  34763  bnj1145  34851  bnj1398  34892  bnj1442  34907  sconnpht  35070  fmla1  35228  goalrlem  35237  goalr  35238  satfv0fvfmla0  35254  fununiq  35605  rdgprc0  35630  bj-substw  36440  bj-opelresdm  36865  poimirlem25  37359  funressnfv  46694  funressnvmo  46696  euoreqb  46758  fcdmvafv2v  46885  dfatbrafv2b  46894  prproropf1olem4  47114  lighneallem2  47214  lindslinindsimp1  47876  fullthinc  48403