Theorem mp3an13 1317

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

Syntax hints:   → wi 4   ∧ w3a 967

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 969

This theorem is referenced by:  pitonnlem1p1  7778  mulid1  7887  addltmul  9084  eluzaddi  9483  fz01en  9978  fznatpl1  10001  expubnd  10502  bernneq  10564  bernneq2  10565  efi4p  11644  efival  11659  cos2tsin  11678  cos01bnd  11685  cos01gt0  11689  dvds0  11732  odd2np1  11795  opoe  11817  gcdid  11904  pythagtriplem4  12177  blssioo  13086  tgioo  13087  rerestcntop  13091  sinperlem  13270  sincosq1sgn  13288  sincosq2sgn  13289  sinq12gt0  13292  cosq14gt0  13294