Theorem mp3an13 1328

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  pitonnlem1p1  7847  mulrid  7956  addltmul  9157  eluzaddi  9556  fz01en  10055  fznatpl1  10078  expubnd  10579  bernneq  10643  bernneq2  10644  efi4p  11727  efival  11742  cos2tsin  11761  cos01bnd  11768  cos01gt0  11772  dvds0  11815  odd2np1  11880  opoe  11902  gcdid  11989  pythagtriplem4  12270  fvpr0o  12765  fvpr1o  12766  blssioo  14084  tgioo  14085  rerestcntop  14089  sinperlem  14268  sincosq1sgn  14286  sincosq2sgn  14287  sinq12gt0  14290  cosq14gt0  14292