Theorem mp3an13 1287

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

Syntax hints:   → wi 4   ∧ w3a 943

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

This theorem depends on definitions:  df-bi 116  df-3an 945

This theorem is referenced by:  pitonnlem1p1  7575  mulid1  7681  addltmul  8854  eluzaddi  9248  fz01en  9720  fznatpl1  9743  expubnd  10237  bernneq  10299  bernneq2  10300  efi4p  11269  efival  11284  cos2tsin  11303  cos01bnd  11310  cos01gt0  11314  dvds0  11350  odd2np1  11412  opoe  11434  gcdid  11516  blssioo  12525  tgioo  12526  rerestcntop  12530