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  7014  op1steq  8015  fpmg  8844  pmresg  8846  pw2f1o  9051  pm54.43  9961  dfac2b  10091  ttukeylem6  10474  gruina  10778  muleqadd  11829  divdiv1  11900  addltmul  12425  elfzp1b  13569  elfzm1b  13570  expp1z  14083  expm1  14084  oddvdsnn0  19481  efgi0  19657  efgi1  19658  fiinbas  22846  opnneissb  23008  fclscf  23919  blssec  24330  iimulcl  24840  itg2lr  25638  blocnilem  30740  lnopmul  31903  opsqrlem6  32081  gsumle  33045  gsumvsca1  33186  gsumvsca2  33187  locfinreflem  33837  fvray  36136  fvline  36139  fneref  36345  poimirlem3  37624  poimirlem16  37637  fdc  37746  linepmap  39776  rmyeq0  42949  omssaxinf2  44985