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  7589  curry1  8040  fsuppunfi  9279  oiid  9434  cantnflt  9569  oemapvali  9581  cnfcom2lem  9598  cfeq0  10154  recmulnq  10862  addgt0sr  11002  mappsrpr  11006  isercolllem2  15575  dvdsaddre2b  16220  ndvdssub  16322  lcmfunsn  16557  imasvscafn  17443  subcidcl  17753  funcoppc  17784  clatleglb  18426  sgrpidmnd  18649  conjsubgen  19165  gagrpid  19208  gaass  19211  cntzssv  19242  cntzi  19243  efgredlemf  19655  abveq0  20735  abvmul  20738  abvtri  20739  cnpimaex  23172  restnlly  23398  fclsopni  23931  xmeteq0  24254  xmettri2  24256  metcnpi  24460  metcnpi2  24461  causs  25226  dvbssntr  25829  dgrlem  26162  dgrlb  26169  precsexlem11  28156  umgredgne  29125  nbgrcl  29315  wlkdlem3  29663  usgr2trlncrct  29786  wwlksonvtx  29835  wwlksnextproplem3  29891  erclwwlknsym  30052  erclwwlkntr  30053  1pthon2v  30135  cycpmco2lem3  33104  idomsubr  33282  elrspunidl  33400  sseqf  34426  subgrwlk  35197  acycgrsubgr  35223  fvineqsneu  37476  pr2el2  43668  rfovcnvf1od  44121  gneispaceel  44260  gneispacess  44262  clnbgrcl  47945  linindslinci  48573  2arymaptfv  48776  f1sn2g  48975  oppf1st2nd  49256  2oppf  49257