Theorem mp3an13 1318

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

Syntax hints:   → wi 4   ∧ w3a 968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  pitonnlem1p1  7787  mulid1  7896  addltmul  9093  eluzaddi  9492  fz01en  9988  fznatpl1  10011  expubnd  10512  bernneq  10575  bernneq2  10576  efi4p  11658  efival  11673  cos2tsin  11692  cos01bnd  11699  cos01gt0  11703  dvds0  11746  odd2np1  11810  opoe  11832  gcdid  11919  pythagtriplem4  12200  blssioo  13185  tgioo  13186  rerestcntop  13190  sinperlem  13369  sincosq1sgn  13387  sincosq2sgn  13388  sinq12gt0  13391  cosq14gt0  13393