Theorem mpanl1 410

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpanl1.1	⊢ φ
mpanl1.2	⊢ (((φ ∧ ψ) ∧ χ) → θ)

Assertion

Ref	Expression
mpanl1	⊢ ((ψ ∧ χ) → θ)

Proof of Theorem mpanl1

Step	Hyp	Ref	Expression
1		mpanl1.1	. . 3 ⊢ φ
2	1	jctl 297	. 2 ⊢ (ψ → (φ ∧ ψ))
3		mpanl1.2	. 2 ⊢ (((φ ∧ ψ) ∧ χ) → θ)
4	2, 3	sylan 267	1 ⊢ ((ψ ∧ χ) → θ)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem is referenced by:  mpanl12  412  ercnv  6063  rec11api  7511  divdiv23apzi  7523  recp1lt1  7646  divgt0i  7657  divge0i  7658  ltreci  7659  lereci  7660  lt2msqi  7661  le2msqi  7662  msq11i  7663  ltdiv23i  7673  fnn0ind  8130  elfzp1b  8729  elfzm1b  8730