mp3an3 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > mp3an3		GIF version

Theorem mp3an3 1266

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

**Hypotheses**
Ref	Expression
mp3an3.1	⊢ χ
mp3an3.2	⊢ ((φ ∧ ψ ∧ χ) → θ)

**Assertion**
Ref	Expression
mp3an3	⊢ ((φ ∧ ψ) → θ)

**Proof of Theorem mp3an3**
Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ χ
2		mp3an3.2	. . 3 ⊢ ((φ ∧ ψ ∧ χ) → θ)
3	2	3expia 1153	. 2 ⊢ ((φ ∧ ψ) → (χ → θ))
4	1, 3	mpi 16	1 ⊢ ((φ ∧ ψ) → θ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 358 ∧ w3a 934

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8

This theorem depends on definitions: df-bi 177 df-an 360 df-3an 936

This theorem is referenced by: mp3an13 1268 mp3an23 1269 mp3anl3 1273 vfinnc 4471 ov 5595 ovmpt2a 5714 ovmpt2 5716 enmap1lem5 6073 ltcpw1pwg 6202 nnltp1c 6262 nnc3n3p1 6278