Theorem mp3an13 1362

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  residfi  7118  pitonnlem1p1  8044  mulrid  8154  addltmul  9359  eluzaddi  9761  fz01en  10261  fznatpl1  10284  expubnd  10830  bernneq  10894  bernneq2  10895  efi4p  12244  efival  12259  cos2tsin  12278  cos01bnd  12285  cos01gt0  12290  dvds0  12333  odd2np1  12400  opoe  12422  gcdid  12523  pythagtriplem4  12807  fvpr0o  13390  fvpr1o  13391  blssioo  15243  tgioo  15244  rerestcntop  15248  rerest  15250  sinperlem  15498  sincosq1sgn  15516  sincosq2sgn  15517  sinq12gt0  15520  cosq14gt0  15522  1sgmprm  15684