Theorem mpanr2 703

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 592	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  7072  op1steq  8074  fpmg  8926  pmresg  8928  pw2f1o  9143  pm54.43  10070  dfac2b  10200  ttukeylem6  10583  gruina  10887  muleqadd  11934  divdiv1  12005  addltmul  12529  elfzp1b  13661  elfzm1b  13662  expp1z  14162  expm1  14163  oddvdsnn0  19586  efgi0  19762  efgi1  19763  fiinbas  22980  opnneissb  23143  fclscf  24054  blssec  24466  iimulcl  24985  itg2lr  25785  blocnilem  30836  lnopmul  31999  opsqrlem6  32177  gsumle  33074  gsumvsca1  33205  gsumvsca2  33206  locfinreflem  33786  fvray  36105  fvline  36108  fneref  36316  poimirlem3  37583  poimirlem16  37596  fdc  37705  linepmap  39732  rmyeq0  42910