Theorem mp3an13 1341

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  residfi  7068  pitonnlem1p1  7994  mulrid  8104  addltmul  9309  eluzaddi  9710  fz01en  10210  fznatpl1  10233  expubnd  10778  bernneq  10842  bernneq2  10843  efi4p  12143  efival  12158  cos2tsin  12177  cos01bnd  12184  cos01gt0  12189  dvds0  12232  odd2np1  12299  opoe  12321  gcdid  12422  pythagtriplem4  12706  fvpr0o  13288  fvpr1o  13289  blssioo  15140  tgioo  15141  rerestcntop  15145  rerest  15147  sinperlem  15395  sincosq1sgn  15413  sincosq2sgn  15414  sinq12gt0  15417  cosq14gt0  15419  1sgmprm  15581