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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  fvreseq1  6859  op1steq  7805  fpmg  8549  pmresg  8551  pw2f1o  8750  pm54.43  9617  dfac2b  9744  ttukeylem6  10128  gruina  10432  muleqadd  11476  divdiv1  11543  addltmul  12066  elfzp1b  13189  elfzm1b  13190  expp1z  13684  expm1  13685  oddvdsnn0  18936  efgi0  19110  efgi1  19111  fiinbas  21849  opnneissb  22011  fclscf  22922  blssec  23333  iimulcl  23834  itg2lr  24628  blocnilem  28885  lnopmul  30048  opsqrlem6  30226  gsumle  31069  gsumvsca1  31198  gsumvsca2  31199  locfinreflem  31504  fvray  34180  fvline  34183  fneref  34276  poimirlem3  35517  poimirlem16  35530  fdc  35640  linepmap  37526  rmyeq0  40478