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  7041  op1steq  8039  fpmg  8875  pmresg  8877  pw2f1o  9080  pm54.43  10006  dfac2b  10133  ttukeylem6  10516  gruina  10821  muleqadd  11876  divdiv1  11944  addltmul  12498  elfzp1b  13648  elfzm1b  13649  expp1z  14167  expm1  14168  oddvdsnn0  19645  efgi0  19821  efgi1  19822  gsumle  20246  fiinbas  23146  opnneissb  23308  fclscf  24219  blssec  24629  iimulcl  25133  itg2lr  25926  blocnilem  31193  lnopmul  32356  opsqrlem6  32534  gsumvsca1  33577  gsumvsca2  33578  locfinreflem  34261  fvray  36654  fvline  36657  fneref  36902  poimirlem3  38315  poimirlem16  38328  fdc  38437  linepmap  40590  rmyeq0  43721  omssaxinf2  45738