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  6977  op1steq  7975  fpmg  8802  pmresg  8804  pw2f1o  9006  pm54.43  9916  dfac2b  10044  ttukeylem6  10427  gruina  10731  muleqadd  11782  divdiv1  11853  addltmul  12378  elfzp1b  13522  elfzm1b  13523  expp1z  14036  expm1  14037  oddvdsnn0  19441  efgi0  19617  efgi1  19618  gsumle  20042  fiinbas  22855  opnneissb  23017  fclscf  23928  blssec  24339  iimulcl  24849  itg2lr  25647  blocnilem  30766  lnopmul  31929  opsqrlem6  32107  gsumvsca1  33181  gsumvsca2  33182  locfinreflem  33809  fvray  36117  fvline  36120  fneref  36326  poimirlem3  37605  poimirlem16  37618  fdc  37727  linepmap  39757  rmyeq0  42929  omssaxinf2  44965