Theorem mpanr2 702

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  fvreseq1  6811  op1steq  7735  fpmg  8434  pmresg  8436  pw2f1o  8624  pm54.43  9431  dfac2b  9558  ttukeylem6  9938  gruina  10242  muleqadd  11286  divdiv1  11353  addltmul  11876  elfzp1b  12987  elfzm1b  12988  expp1z  13481  expm1  13482  oddvdsnn0  18674  efgi0  18848  efgi1  18849  fiinbas  21562  opnneissb  21724  fclscf  22635  blssec  23047  iimulcl  23543  itg2lr  24333  blocnilem  28583  lnopmul  29746  opsqrlem6  29924  gsumle  30727  gsumvsca1  30856  gsumvsca2  30857  locfinreflem  31106  fvray  33604  fvline  33607  fneref  33700  poimirlem3  34897  poimirlem16  34910  fdc  35022  linepmap  36913  rmyeq0  39557