Theorem mpanr2 702

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fvreseq1  6809  op1steq  7733  fpmg  8432  pmresg  8434  pw2f1o  8622  pm54.43  9429  dfac2b  9556  ttukeylem6  9936  gruina  10240  muleqadd  11284  divdiv1  11351  addltmul  11874  elfzp1b  12985  elfzm1b  12986  expp1z  13479  expm1  13480  oddvdsnn0  18672  efgi0  18846  efgi1  18847  fiinbas  21560  opnneissb  21722  fclscf  22633  blssec  23045  iimulcl  23541  itg2lr  24331  blocnilem  28581  lnopmul  29744  opsqrlem6  29922  gsumle  30725  gsumvsca1  30854  gsumvsca2  30855  locfinreflem  31104  fvray  33602  fvline  33605  fneref  33698  poimirlem3  34910  poimirlem16  34923  fdc  35035  linepmap  36926  rmyeq0  39570