Theorem mpanr2 719

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  fvreseq1  6284  op1steq  7170  fpmg  7843  pmresg  7845  pw2f1o  8025  pm54.43  8786  dfac2  8913  ttukeylem6  9296  gruina  9600  muleqadd  10631  divdiv1  10696  addltmul  11228  elfzp1b  12374  elfzm1b  12375  expp1z  12865  expm1  12866  oddvdsnn0  17903  efgi0  18073  efgi1  18074  fiinbas  20696  opnneissb  20858  fclscf  21769  blssec  22180  iimulcl  22676  itg2lr  23437  blocnilem  27547  lnopmul  28714  opsqrlem6  28892  gsumle  29606  gsumvsca1  29609  gsumvsca2  29610  locfinreflem  29731  fvray  31943  fvline  31946  fneref  32040  poimirlem3  33083  poimirlem16  33096  fdc  33212  linepmap  34580  rmyeq0  37039