Theorem mpanr2 716

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

Syntax hints:   → wi 4   ∧ wa 400

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  fvreseq1  7036  op1steq  8031  fpmg  8867  pmresg  8869  pw2f1o  9071  pm54.43  9988  dfac2b  10115  ttukeylem6  10499  gruina  10804  muleqadd  11859  divdiv1  11927  addltmul  12481  elfzp1b  13631  elfzm1b  13632  expp1z  14149  expm1  14150  oddvdsnn0  19615  efgi0  19791  efgi1  19792  gsumle  20216  fiinbas  23090  opnneissb  23252  fclscf  24163  blssec  24573  iimulcl  25077  itg2lr  25870  blocnilem  31137  lnopmul  32300  opsqrlem6  32478  gsumvsca1  33527  gsumvsca2  33528  locfinreflem  34211  fvray  36614  fvline  36617  fneref  36842  poimirlem3  38255  poimirlem16  38268  fdc  38377  linepmap  40530  rmyeq0  43663  omssaxinf2  45680