Theorem mpanr2 700

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

This theorem is referenced by:  fvreseq1  6898  op1steq  7848  fpmg  8614  pmresg  8616  pw2f1o  8817  pm54.43  9690  dfac2b  9817  ttukeylem6  10201  gruina  10505  muleqadd  11549  divdiv1  11616  addltmul  12139  elfzp1b  13262  elfzm1b  13263  expp1z  13760  expm1  13761  oddvdsnn0  19067  efgi0  19241  efgi1  19242  fiinbas  22010  opnneissb  22173  fclscf  23084  blssec  23496  iimulcl  24006  itg2lr  24800  blocnilem  29067  lnopmul  30230  opsqrlem6  30408  gsumle  31252  gsumvsca1  31381  gsumvsca2  31382  locfinreflem  31692  fvray  34370  fvline  34373  fneref  34466  poimirlem3  35707  poimirlem16  35720  fdc  35830  linepmap  37716  rmyeq0  40691