Theorem mpanr2 436

Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpanr2.1	⊢ 𝜒
mpanr2.2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
mpanr2	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mpanr2

Step	Hyp	Ref	Expression
1		mpanr2.1	. . 3 ⊢ 𝜒
2	1	jctr 313	. 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒))
3		mpanr2.2	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	sylan2 284	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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 is referenced by:  op1steq  6155  fpmg  6648  pmresg  6650  pm54.43  7154  prarloclemarch2  7368  prarloclemlt  7442  prsradd  7735  muleqadd  8573  divdivap1  8627  addltmul  9101  elfzp1b  10040  elfzm1b  10041  expp1zap  10512  expm1ap  10513  fiinbas  12800  opnneissb  12908  blssec  13191