Theorem mp3an13 1364

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  residfi  7139  pitonnlem1p1  8066  mulrid  8176  addltmul  9381  eluzaddi  9783  fz01en  10288  fznatpl1  10311  expubnd  10859  bernneq  10923  bernneq2  10924  efi4p  12296  efival  12311  cos2tsin  12330  cos01bnd  12337  cos01gt0  12342  dvds0  12385  odd2np1  12452  opoe  12474  gcdid  12575  pythagtriplem4  12859  fvpr0o  13442  fvpr1o  13443  blssioo  15296  tgioo  15297  rerestcntop  15301  rerest  15303  sinperlem  15551  sincosq1sgn  15569  sincosq2sgn  15570  sinq12gt0  15573  cosq14gt0  15575  1sgmprm  15737  konigsberg  16363