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  7820  mulid1  7929  addltmul  9128  eluzaddi  9527  fz01en  10023  fznatpl1  10046  expubnd  10547  bernneq  10610  bernneq2  10611  efi4p  11693  efival  11708  cos2tsin  11727  cos01bnd  11734  cos01gt0  11738  dvds0  11781  odd2np1  11845  opoe  11867  gcdid  11954  pythagtriplem4  12235  blssioo  13625  tgioo  13626  rerestcntop  13630  sinperlem  13809  sincosq1sgn  13827  sincosq2sgn  13828  sinq12gt0  13831  cosq14gt0  13833