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  3844  dfss2  3916  solin  5554  xpidtr  6073  f1ssres  6731  fvn0ssdmfun  7013  f1veqaeq  7196  f1opw  7608  resf1extb  7870  fprlem1  8236  ixpn0  8860  domunsncan  8997  phplem2  9121  php3  9125  infsupprpr  9397  frrlem15  9657  dfac9  10035  ltxrlt  11190  znegcl  12513  zltaddlt1le  13407  injresinj  13693  fsuppmapnn0fiubex  13901  pfxccatin12lem3  14641  repswswrd  14693  oddnn02np1  16261  sumeven  16300  ncoprmgcdne1b  16563  dvdsprmpweqnn  16799  prmodvdslcmf  16961  sgrpass  18635  symgextf1  19335  fvcosymgeq  19343  ricgic  20424  zringndrg  21407  evlslem4  22012  scmatf1  22447  pmatcoe1fsupp  22617  t1sncld  23242  regsep  23250  nrmsep3  23271  cmpsublem  23315  ufilss  23821  fclscf  23941  ncvsprp  25080  ncvsm1  25082  ncvsdif  25083  ncvspi  25084  ncvspds  25089  mblsplit  25461  mbfdm  25555  fta1glem1  26101  aaliou2  26276  dvloglem  26585  lgsqrlem4  27288  2sqnn0  27377  ausgrusgrb  29145  fusgredgfi  29305  vtxdumgrval  29467  vtxdginducedm1lem4  29523  umgrn1cycl  29787  hashecclwwlkn1  30059  umgrhashecclwwlk  30060  0spth  30108  eucrctshift  30225  frcond1  30248  2pthfrgr  30266  frgrncvvdeqlem7  30287  frgrncvvdeq  30291  frgrwopreglem3  30296  frgrwopreglem5lem  30302  frgr2wwlk1  30311  numclwwlk1lem2f1  30339  hhcms  31185  stcltr1i  32256  chpssati  32345  bnj570  34938  bnj1145  35026  bnj1398  35067  bnj1442  35082  sconnpht  35294  fmla1  35452  goalrlem  35461  goalr  35462  satfv0fvfmla0  35478  fununiq  35834  rdgprc0  35856  bj-substw  36787  bj-opelresdm  37210  poimirlem25  37705  funressnfv  47167  funressnvmo  47169  euoreqb  47233  fcdmvafv2v  47360  dfatbrafv2b  47369  prproropf1olem4  47630  lighneallem2  47730  grlimgrtrilem2  48126  pgnioedg1  48232  pgnioedg2  48233  pgnioedg3  48234  pgnioedg4  48235  pgnioedg5  48236  pgnbgreunbgrlem2lem1  48238  pgnbgreunbgrlem2lem2  48239  pgnbgreunbgrlem2lem3  48240  pgnbgreunbgrlem5lem1  48244  pgnbgreunbgrlem5lem2  48245  pgnbgreunbgrlem5lem3  48246  lindslinindsimp1  48582  fullthinc  49575