Theorem mpanr2 701

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  fvreseq1  6966  op1steq  7935  fpmg  8719  pmresg  8721  pw2f1o  8934  pm54.43  9850  dfac2b  9979  ttukeylem6  10363  gruina  10667  muleqadd  11712  divdiv1  11779  addltmul  12302  elfzp1b  13426  elfzm1b  13427  expp1z  13925  expm1  13926  oddvdsnn0  19240  efgi0  19413  efgi1  19414  fiinbas  22200  opnneissb  22363  fclscf  23274  blssec  23686  iimulcl  24198  itg2lr  24993  blocnilem  29395  lnopmul  30558  opsqrlem6  30736  gsumle  31578  gsumvsca1  31707  gsumvsca2  31708  locfinreflem  32029  fvray  34534  fvline  34537  fneref  34630  poimirlem3  35878  poimirlem16  35891  fdc  36001  linepmap  38036  rmyeq0  41026