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  7039  op1steq  8046  fpmg  8900  pmresg  8902  pw2f1o  9105  pm54.43  10086  dfac2b  10213  ttukeylem6  10596  gruina  10907  muleqadd  11964  divdiv1  12032  addltmul  12586  elfzp1b  13739  elfzm1b  13740  expp1z  14258  expm1  14259  oddvdsnn0  19764  efgi0  19940  efgi1  19941  gsumle  20365  fiinbas  23276  opnneissb  23438  fclscf  24350  blssec  24760  iimulcl  25264  itg2lr  26057  blocnilem  31412  lnopmul  32575  opsqrlem6  32753  gsumvsca1  33834  gsumvsca2  33835  locfinreflem  34519  fvray  36999  fvline  37002  fneref  37231  poimirlem3  38635  poimirlem16  38648  fdc  38773  linepmap  40926  rmyeq0  44054  omssaxinf2  46072