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  7059  op1steq  8057  fpmg  8907  pmresg  8909  pw2f1o  9116  pm54.43  10039  dfac2b  10169  ttukeylem6  10552  gruina  10856  muleqadd  11905  divdiv1  11976  addltmul  12500  elfzp1b  13638  elfzm1b  13639  expp1z  14149  expm1  14150  oddvdsnn0  19577  efgi0  19753  efgi1  19754  fiinbas  22975  opnneissb  23138  fclscf  24049  blssec  24461  iimulcl  24980  itg2lr  25780  blocnilem  30833  lnopmul  31996  opsqrlem6  32174  gsumle  33084  gsumvsca1  33215  gsumvsca2  33216  locfinreflem  33801  fvray  36123  fvline  36126  fneref  36333  poimirlem3  37610  poimirlem16  37623  fdc  37732  linepmap  39758  rmyeq0  42942