Theorem mp3an13 1328

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 1326	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan 424	1 ⊢ (𝜓 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  pitonnlem1p1  7844  mulrid  7953  addltmul  9154  eluzaddi  9553  fz01en  10052  fznatpl1  10075  expubnd  10576  bernneq  10640  bernneq2  10641  efi4p  11724  efival  11739  cos2tsin  11758  cos01bnd  11765  cos01gt0  11769  dvds0  11812  odd2np1  11877  opoe  11899  gcdid  11986  pythagtriplem4  12267  fvpr0o  12759  fvpr1o  12760  blssioo  14015  tgioo  14016  rerestcntop  14020  sinperlem  14199  sincosq1sgn  14217  sincosq2sgn  14218  sinq12gt0  14221  cosq14gt0  14223