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  7840  mulrid  7949  addltmul  9149  eluzaddi  9548  fz01en  10046  fznatpl1  10069  expubnd  10570  bernneq  10633  bernneq2  10634  efi4p  11716  efival  11731  cos2tsin  11750  cos01bnd  11757  cos01gt0  11761  dvds0  11804  odd2np1  11868  opoe  11890  gcdid  11977  pythagtriplem4  12258  blssioo  13827  tgioo  13828  rerestcntop  13832  sinperlem  14011  sincosq1sgn  14029  sincosq2sgn  14030  sinq12gt0  14033  cosq14gt0  14035