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  7254  pitonnlem1p1  8214  mulrid  8324  addltmul  9547  eluzaddi  9959  fz01en  10470  fznatpl1  10494  expubnd  11048  bernneq  11113  bernneq2  11114  efi4p  12503  efival  12518  cos2tsin  12537  cos01bnd  12544  cos01gt0  12549  dvds0  12592  odd2np1  12659  opoe  12681  gcdid  12782  pythagtriplem4  13070  fvpr0o  13715  fvpr1o  13716  blssioo  15745  tgioo  15746  rerestcntop  15750  rerest  15752  sinperlem  16001  sincosq1sgn  16019  sincosq2sgn  16020  sinq12gt0  16023  cosq14gt0  16025  1sgmprm  16249  ppiqub  16254  chtublem  16256  chtqub  16257  bcp1ctr  16267  bpos1lem  16270  bposlem2  16273  bposlem3  16274  bposlem4  16275  bposlem5  16276  bposlem6  16277  bposlem7  16278  bposlem9  16280  konigsberg  16900