Theorem mpanr2 717

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 534	. 2 ⊢ (𝜓 → (𝜓 ∧ 𝜒))
3		mpanr2.2	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	2, 3	sylan2 605	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fvreseq1  7064  op1steq  8072  fpmg  8927  pmresg  8929  pw2f1o  9132  pm54.43  10112  dfac2b  10239  ttukeylem6  10622  gruina  10933  muleqadd  11990  divdiv1  12058  addltmul  12612  elfzp1b  13765  elfzm1b  13766  expp1z  14284  expm1  14285  oddvdsnn0  19791  efgi0  19967  efgi1  19968  gsumle  20392  fiinbas  23303  opnneissb  23465  fclscf  24377  blssec  24787  iimulcl  25291  itg2lr  26084  blocnilem  31439  lnopmul  32602  opsqrlem6  32780  gsumvsca1  33863  gsumvsca2  33864  locfinreflem  34555  fvray  37097  fvline  37100  fneref  37329  poimirlem3  38746  poimirlem16  38759  fdc  38882  linepmap  41035  rmyeq0  44164  omssaxinf2  46184