Theorem simpl2im 503

Description: Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)

Hypotheses

Ref	Expression
simpl2im.1	⊢ (𝜑 → (𝜓 ∧ 𝜒))
simpl2im.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
simpl2im	⊢ (𝜑 → 𝜃)

Proof of Theorem simpl2im

Step	Hyp	Ref	Expression
1		simpl2im.1	. . 3 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2	1	simprd 495	. 2 ⊢ (𝜑 → 𝜒)
3		simpl2im.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ 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:  caovmo  7644  curry1  8103  fsuppunfi  9400  oiid  9555  cantnflt  9686  oemapvali  9698  cnfcom2lem  9715  cfeq0  10270  recmulnq  10978  addgt0sr  11118  mappsrpr  11122  isercolllem2  15682  dvdsaddre2b  16326  ndvdssub  16428  lcmfunsn  16663  imasvscafn  17551  subcidcl  17857  funcoppc  17888  clatleglb  18528  sgrpidmnd  18717  conjsubgen  19234  gagrpid  19277  gaass  19280  cntzssv  19311  cntzi  19312  efgredlemf  19722  abveq0  20778  abvmul  20781  abvtri  20782  cnpimaex  23194  restnlly  23420  fclsopni  23953  xmeteq0  24277  xmettri2  24279  metcnpi  24483  metcnpi2  24484  causs  25250  dvbssntr  25853  dgrlem  26186  dgrlb  26193  precsexlem11  28171  umgredgne  29124  nbgrcl  29314  wlkdlem3  29664  usgr2trlncrct  29788  wwlksonvtx  29837  wwlksnextproplem3  29893  erclwwlknsym  30051  erclwwlkntr  30052  1pthon2v  30134  cycpmco2lem3  33139  idomsubr  33303  elrspunidl  33443  sseqf  34424  subgrwlk  35154  acycgrsubgr  35180  fvineqsneu  37429  pr2el2  43575  rfovcnvf1od  44028  gneispaceel  44167  gneispacess  44169  clnbgrcl  47835  linindslinci  48424  2arymaptfv  48631  f1sn2g  48829  oppf1st2nd  49079  2oppf  49080