Theorem mpanr2 705

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 594	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  6993  op1steq  7987  fpmg  8818  pmresg  8820  pw2f1o  9022  pm54.43  9925  dfac2b  10053  ttukeylem6  10436  gruina  10741  muleqadd  11793  divdiv1  11864  addltmul  12389  elfzp1b  13529  elfzm1b  13530  expp1z  14046  expm1  14047  oddvdsnn0  19485  efgi0  19661  efgi1  19662  gsumle  20086  fiinbas  22908  opnneissb  23070  fclscf  23981  blssec  24391  iimulcl  24901  itg2lr  25699  blocnilem  30891  lnopmul  32054  opsqrlem6  32232  gsumvsca1  33319  gsumvsca2  33320  locfinreflem  34017  fvray  36354  fvline  36357  fneref  36563  poimirlem3  37871  poimirlem16  37884  fdc  37993  linepmap  40148  rmyeq0  43307  omssaxinf2  45341