Theorem mpanr2 716

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  fvreseq1  6226  op1steq  7101  fpmg  7769  pmresg  7771  pw2f1o  7950  pm54.43  8709  dfac2  8836  ttukeylem6  9219  gruina  9519  muleqadd  10550  divdiv1  10615  addltmul  11145  elfzp1b  12286  elfzm1b  12287  expp1z  12771  expm1  12772  oddvdsnn0  17786  efgi0  17956  efgi1  17957  fiinbas  20567  opnneissb  20728  fclscf  21639  blssec  22050  iimulcl  22544  itg2lr  23303  blocnilem  27043  lnopmul  28210  opsqrlem6  28388  gsumle  29110  gsumvsca1  29113  gsumvsca2  29114  locfinreflem  29235  fvray  31418  fvline  31421  fneref  31515  poimirlem3  32582  poimirlem16  32595  fdc  32711  linepmap  34079  rmyeq0  36538