Theorem mp3an13 1306

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

Syntax hints:   → wi 4   ∧ w3a 962

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

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

This theorem is referenced by:  pitonnlem1p1  7647  mulid1  7756  addltmul  8949  eluzaddi  9345  fz01en  9826  fznatpl1  9849  expubnd  10343  bernneq  10405  bernneq2  10406  efi4p  11413  efival  11428  cos2tsin  11447  cos01bnd  11454  cos01gt0  11458  dvds0  11497  odd2np1  11559  opoe  11581  gcdid  11663  blssioo  12703  tgioo  12704  rerestcntop  12708  sinperlem  12878  sincosq1sgn  12896  sincosq2sgn  12897  sinq12gt0  12900  cosq14gt0  12902