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  3863  dfss2  3935  solin  5576  xpidtr  6098  funimaexgOLD  6607  f1ssres  6766  fvn0ssdmfun  7049  f1veqaeq  7234  f1opw  7648  resf1extb  7913  fprlem1  8282  ixpn0  8906  domunsncan  9046  phplem2  9175  php3  9179  infsupprpr  9464  frrlem15  9717  dfac9  10097  ltxrlt  11251  znegcl  12575  zltaddlt1le  13473  injresinj  13756  fsuppmapnn0fiubex  13964  pfxccatin12lem3  14704  repswswrd  14756  oddnn02np1  16325  sumeven  16364  ncoprmgcdne1b  16627  dvdsprmpweqnn  16863  prmodvdslcmf  17025  sgrpass  18659  symgextf1  19358  fvcosymgeq  19366  ricgic  20423  zringndrg  21385  evlslem4  21990  scmatf1  22425  pmatcoe1fsupp  22595  t1sncld  23220  regsep  23228  nrmsep3  23249  cmpsublem  23293  ufilss  23799  fclscf  23919  ncvsprp  25059  ncvsm1  25061  ncvsdif  25062  ncvspi  25063  ncvspds  25068  mblsplit  25440  mbfdm  25534  fta1glem1  26080  aaliou2  26255  dvloglem  26564  lgsqrlem4  27267  2sqnn0  27356  ausgrusgrb  29099  fusgredgfi  29259  vtxdumgrval  29421  vtxdginducedm1lem4  29477  umgrn1cycl  29744  hashecclwwlkn1  30013  umgrhashecclwwlk  30014  0spth  30062  eucrctshift  30179  frcond1  30202  2pthfrgr  30220  frgrncvvdeqlem7  30241  frgrncvvdeq  30245  frgrwopreglem3  30250  frgrwopreglem5lem  30256  frgr2wwlk1  30265  numclwwlk1lem2f1  30293  hhcms  31139  stcltr1i  32210  bnj570  34902  bnj1145  34990  bnj1398  35031  bnj1442  35046  sconnpht  35223  fmla1  35381  goalrlem  35390  goalr  35391  satfv0fvfmla0  35407  fununiq  35763  rdgprc0  35788  bj-substw  36717  bj-opelresdm  37140  poimirlem25  37646  funressnfv  47048  funressnvmo  47050  euoreqb  47114  fcdmvafv2v  47241  dfatbrafv2b  47250  prproropf1olem4  47511  lighneallem2  47611  grlimgrtrilem2  47998  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  lindslinindsimp1  48450  fullthinc  49443