Theorem mp3an13 1365

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  residfi  7182  pitonnlem1p1  8126  mulrid  8236  addltmul  9440  eluzaddi  9844  fz01en  10350  fznatpl1  10373  expubnd  10921  bernneq  10985  bernneq2  10986  efi4p  12358  efival  12373  cos2tsin  12392  cos01bnd  12399  cos01gt0  12404  dvds0  12447  odd2np1  12514  opoe  12536  gcdid  12637  pythagtriplem4  12921  fvpr0o  13504  fvpr1o  13505  blssioo  15364  tgioo  15365  rerestcntop  15369  rerest  15371  sinperlem  15619  sincosq1sgn  15637  sincosq2sgn  15638  sinq12gt0  15641  cosq14gt0  15643  1sgmprm  15808  konigsberg  16434