Theorem mpanr2 704

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 593	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  6984  op1steq  7977  fpmg  8806  pmresg  8808  pw2f1o  9010  pm54.43  9913  dfac2b  10041  ttukeylem6  10424  gruina  10729  muleqadd  11781  divdiv1  11852  addltmul  12377  elfzp1b  13517  elfzm1b  13518  expp1z  14034  expm1  14035  oddvdsnn0  19473  efgi0  19649  efgi1  19650  gsumle  20074  fiinbas  22896  opnneissb  23058  fclscf  23969  blssec  24379  iimulcl  24889  itg2lr  25687  blocnilem  30879  lnopmul  32042  opsqrlem6  32220  gsumvsca1  33308  gsumvsca2  33309  locfinreflem  33997  fvray  36335  fvline  36338  fneref  36544  poimirlem3  37824  poimirlem16  37837  fdc  37946  linepmap  40035  rmyeq0  43195  omssaxinf2  45229