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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  fvreseq1  7041  op1steq  8019  fpmg  8862  pmresg  8864  pw2f1o  9077  pm54.43  9996  dfac2b  10125  ttukeylem6  10509  gruina  10813  muleqadd  11858  divdiv1  11925  addltmul  12448  elfzp1b  13578  elfzm1b  13579  expp1z  14077  expm1  14078  oddvdsnn0  19412  efgi0  19588  efgi1  19589  fiinbas  22455  opnneissb  22618  fclscf  23529  blssec  23941  iimulcl  24453  itg2lr  25248  blocnilem  30088  lnopmul  31251  opsqrlem6  31429  gsumle  32273  gsumvsca1  32402  gsumvsca2  32403  locfinreflem  32851  fvray  35144  fvline  35147  fneref  35283  poimirlem3  36539  poimirlem16  36552  fdc  36661  linepmap  38694  rmyeq0  41740