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  7595  curry1  8046  fsuppunfi  9291  oiid  9446  cantnflt  9581  oemapvali  9593  cnfcom2lem  9610  cfeq0  10166  recmulnq  10875  addgt0sr  11015  mappsrpr  11019  isercolllem2  15589  dvdsaddre2b  16234  ndvdssub  16336  lcmfunsn  16571  imasvscafn  17458  subcidcl  17768  funcoppc  17799  clatleglb  18441  sgrpidmnd  18664  conjsubgen  19180  gagrpid  19223  gaass  19226  cntzssv  19257  cntzi  19258  efgredlemf  19670  abveq0  20751  abvmul  20754  abvtri  20755  cnpimaex  23200  restnlly  23426  fclsopni  23959  xmeteq0  24282  xmettri2  24284  metcnpi  24488  metcnpi2  24489  causs  25254  dvbssntr  25857  dgrlem  26190  dgrlb  26197  precsexlem11  28213  umgredgne  29218  nbgrcl  29408  wlkdlem3  29756  usgr2trlncrct  29879  wwlksonvtx  29928  wwlksnextproplem3  29984  erclwwlknsym  30145  erclwwlkntr  30146  1pthon2v  30228  cycpmco2lem3  33210  idomsubr  33391  elrspunidl  33509  sseqf  34549  subgrwlk  35326  acycgrsubgr  35352  fvineqsneu  37612  pr2el2  43788  rfovcnvf1od  44241  gneispaceel  44380  gneispacess  44382  clnbgrcl  48063  linindslinci  48690  2arymaptfv  48893  f1sn2g  49092  oppf1st2nd  49372  2oppf  49373