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  7011  op1steq  8012  fpmg  8841  pmresg  8843  pw2f1o  9046  pm54.43  9954  dfac2b  10084  ttukeylem6  10467  gruina  10771  muleqadd  11822  divdiv1  11893  addltmul  12418  elfzp1b  13562  elfzm1b  13563  expp1z  14076  expm1  14077  oddvdsnn0  19474  efgi0  19650  efgi1  19651  fiinbas  22839  opnneissb  23001  fclscf  23912  blssec  24323  iimulcl  24833  itg2lr  25631  blocnilem  30733  lnopmul  31896  opsqrlem6  32074  gsumle  33038  gsumvsca1  33179  gsumvsca2  33180  locfinreflem  33830  fvray  36129  fvline  36132  fneref  36338  poimirlem3  37617  poimirlem16  37630  fdc  37739  linepmap  39769  rmyeq0  42942  omssaxinf2  44978