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  6991  op1steq  7986  fpmg  8816  pmresg  8818  pw2f1o  9020  pm54.43  9925  dfac2b  10053  ttukeylem6  10436  gruina  10741  muleqadd  11794  divdiv1  11866  addltmul  12413  elfzp1b  13555  elfzm1b  13556  expp1z  14073  expm1  14074  oddvdsnn0  19519  efgi0  19695  efgi1  19696  gsumle  20120  fiinbas  22917  opnneissb  23079  fclscf  23990  blssec  24400  iimulcl  24904  itg2lr  25697  blocnilem  30875  lnopmul  32038  opsqrlem6  32216  gsumvsca1  33287  gsumvsca2  33288  locfinreflem  33984  fvray  36323  fvline  36326  fneref  36532  poimirlem3  37944  poimirlem16  37957  fdc  38066  linepmap  40221  rmyeq0  43381  omssaxinf2  45415