Theorem mpanr2 705

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 594	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  6985  op1steq  7979  fpmg  8809  pmresg  8811  pw2f1o  9013  pm54.43  9916  dfac2b  10044  ttukeylem6  10427  gruina  10732  muleqadd  11785  divdiv1  11857  addltmul  12404  elfzp1b  13546  elfzm1b  13547  expp1z  14064  expm1  14065  oddvdsnn0  19510  efgi0  19686  efgi1  19687  gsumle  20111  fiinbas  22927  opnneissb  23089  fclscf  24000  blssec  24410  iimulcl  24914  itg2lr  25707  blocnilem  30890  lnopmul  32053  opsqrlem6  32231  gsumvsca1  33302  gsumvsca2  33303  locfinreflem  34000  fvray  36339  fvline  36342  fneref  36548  poimirlem3  37958  poimirlem16  37971  fdc  38080  linepmap  40235  rmyeq0  43399  omssaxinf2  45433