Theorem mpanl1 706

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

Ref	Expression
mpanl1.1	⊢ 𝜑
mpanl1.2	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpanl1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mpanl1

Step	Hyp	Ref	Expression
1		mpanl1.1	. . 3 ⊢ 𝜑
2	1	jctl 528	. 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓))
3		mpanl1.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 586	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  mpanl12  708  frc  5588  oeoelem  8531  ercnv  8662  frfi  9192  fin23lem23  10246  divdiv23zi  11906  recp1lt1  12052  divgt0i  12062  divge0i  12063  ltreci  12064  lereci  12065  lt2msqi  12066  le2msqi  12067  msq11i  12068  ltdiv23i  12078  fnn0ind  12626  elfzp1b  13553  elfzm1b  13554  sqrt11i  15345  sqrtmuli  15346  sqrtmsq2i  15348  sqrtlei  15349  sqrtlti  15350  fsum  15680  fprod  15904  blometi  30899  spansnm0i  31746  lnopli  32064  lnfnli  32136  opsqrlem1  32236  opsqrlem6  32241  mdslmd3i  32428  atordi  32480  mdsymlem1  32499  gsummpt2co  33136  finxpreclem4  37763  ptrecube  37994  fdc  38119  prter3  39381