Theorem mpanr2 704

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  fvreseq1  7058  op1steq  8059  fpmg  8909  pmresg  8911  pw2f1o  9118  pm54.43  10042  dfac2b  10172  ttukeylem6  10555  gruina  10859  muleqadd  11908  divdiv1  11979  addltmul  12504  elfzp1b  13642  elfzm1b  13643  expp1z  14153  expm1  14154  oddvdsnn0  19563  efgi0  19739  efgi1  19740  fiinbas  22960  opnneissb  23123  fclscf  24034  blssec  24446  iimulcl  24967  itg2lr  25766  blocnilem  30824  lnopmul  31987  opsqrlem6  32165  gsumle  33102  gsumvsca1  33233  gsumvsca2  33234  locfinreflem  33840  fvray  36143  fvline  36146  fneref  36352  poimirlem3  37631  poimirlem16  37644  fdc  37753  linepmap  39778  rmyeq0  42970  omssaxinf2  45010