Theorem mpanr2 716

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401

This theorem is used by:  fvreseq1  7034  op1steq  8028  fpmg  8864  pmresg  8866  pw2f1o  9068  pm54.43  9994  dfac2b  10121  ttukeylem6  10504  gruina  10809  muleqadd  11864  divdiv1  11932  addltmul  12486  elfzp1b  13636  elfzm1b  13637  expp1z  14154  expm1  14155  oddvdsnn0  19620  efgi0  19796  efgi1  19797  gsumle  20221  fiinbas  23120  opnneissb  23282  fclscf  24193  blssec  24603  iimulcl  25107  itg2lr  25900  blocnilem  31167  lnopmul  32330  opsqrlem6  32508  gsumvsca1  33555  gsumvsca2  33556  locfinreflem  34239  fvray  36641  fvline  36644  fneref  36889  poimirlem3  38302  poimirlem16  38315  fdc  38424  linepmap  40577  rmyeq0  43708  omssaxinf2  45725