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  11047  bernneq  11112  bernneq2  11113  efi4p  12502  efival  12517  cos2tsin  12536  cos01bnd  12543  cos01gt0  12548  dvds0  12591  odd2np1  12658  opoe  12680  gcdid  12781  pythagtriplem4  13069  fvpr0o  13713  fvpr1o  13714  blssioo  15706  tgioo  15707  rerestcntop  15711  rerest  15713  sinperlem  15962  sincosq1sgn  15980  sincosq2sgn  15981  sinq12gt0  15984  cosq14gt0  15986  1sgmprm  16210  ppiqub  16215  chtublem  16217  chtqub  16218  bcp1ctr  16228  bpos1lem  16231  bposlem2  16234  bposlem3  16235  bposlem4  16236  bposlem5  16237  konigsberg  16856