Theorem mp3an13 1341

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

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

Assertion

Ref	Expression
mp3an13	⊢ (𝜓 → 𝜃)

Proof of Theorem mp3an13

Step	Hyp	Ref	Expression
1		mp3an13.1	. 2 ⊢ 𝜑
2		mp3an13.2	. . 3 ⊢ 𝜒
3		mp3an13.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1339	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 424	1 ⊢ (𝜓 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  residfi  7044  pitonnlem1p1  7961  mulrid  8071  addltmul  9276  eluzaddi  9677  fz01en  10177  fznatpl1  10200  expubnd  10743  bernneq  10807  bernneq2  10808  efi4p  12061  efival  12076  cos2tsin  12095  cos01bnd  12102  cos01gt0  12107  dvds0  12150  odd2np1  12217  opoe  12239  gcdid  12340  pythagtriplem4  12624  fvpr0o  13206  fvpr1o  13207  blssioo  15058  tgioo  15059  rerestcntop  15063  rerest  15065  sinperlem  15313  sincosq1sgn  15331  sincosq2sgn  15332  sinq12gt0  15335  cosq14gt0  15337  1sgmprm  15499