Theorem simpl2im 512

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 500	. 2 ⊢ (𝜑 → 𝜒)
3		simpl2im.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 18	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  caovmo  7647  curry1  8098  fsuppunfi  9347  oiid  9502  cantnflt  9640  oemapvali  9652  cnfcom2lem  9669  cfeq0  10239  recmulnq  10948  addgt0sr  11088  mappsrpr  11092  isercolllem2  15716  dvdsaddre2b  16364  ndvdssub  16466  lcmfunsn  16701  imasvscafn  17590  subcidcl  17900  funcoppc  17931  clatleglb  18573  sgrpidmnd  18796  conjsubgen  19320  gagrpid  19363  gaass  19366  cntzssv  19397  cntzi  19398  efgredlemf  19810  abveq0  20900  abvmul  20903  abvtri  20904  cnpimaex  23392  restnlly  23618  fclsopni  24151  xmeteq0  24474  xmettri2  24476  metcnpi  24680  metcnpi2  24681  causs  25436  dvbssntr  26038  dgrlem  26365  dgrlb  26372  precsexlem11  28386  umgredgne  29461  nbgrcl  29651  wlkdlem3  29998  usgr2trlncrct  30121  wwlksonvtx  30170  wwlksnextproplem3  30226  erclwwlknsym  30387  erclwwlkntr  30388  1pthon2v  30470  cycpmco2lem3  33414  idomsubr  33596  elrspunidl  33702  sseqf  34748  subgrwlk  35578  acycgrsubgr  35604  fvineqsneu  38001  pr2el2  44225  rfovcnvf1od  44678  gneispaceel  44817  gneispacess  44819  clnbgrcl  48531  linindslinci  49173  2arymaptfv  49376  f1sn2g  49574  oppf1st2nd  49854  2oppf  49855