Theorem mp3an13 1369

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  residfi  7260  pitonnlem1p1  8219  mulrid  8329  addltmul  9553  eluzaddi  9964  fz01en  10475  fznatpl1  10499  expubnd  11053  bernneq  11118  bernneq2  11119  efi4p  12508  efival  12523  cos2tsin  12542  cos01bnd  12549  cos01gt0  12554  dvds0  12597  odd2np1  12664  opoe  12686  gcdid  12787  pythagtriplem4  13075  fvpr0o  13720  fvpr1o  13721  blssioo  15796  tgioo  15797  rerestcntop  15801  rerest  15803  sinperlem  16052  sincosq1sgn  16070  sincosq2sgn  16071  sinq12gt0  16074  cosq14gt0  16076  1sgmprm  16305  ppiqub  16310  chtublem  16312  chtqub  16313  bcp1ctr  16323  bpos1lem  16326  bposlem2  16329  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem7  16334  bposlem9  16336  konigsberg  16956