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  6127  rec11api  7729  divdiv23apzi  7741  recp1lt1  7865  divgt0i  7876  divge0i  7877  ltreci  7878  lereci  7879  lt2msqi  7880  le2msqi  7881  msq11i  7882  ltdiv23i  7892  fnn0ind  8354  elfzp1b  8959  elfzm1b  8960  sqrt11i  9728  sqrtmuli  9729  sqrtmsq2i  9731  sqrtlei  9732  sqrtlti  9733