Theorem mpanl1 701

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 523	. 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓))
3		mpanl1.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 581	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:  mpanl12  703  frc  5594  oeoelem  8534  ercnv  8665  frfi  9195  fin23lem23  10248  divdiv23zi  11908  recp1lt1  12054  divgt0i  12064  divge0i  12065  ltreci  12066  lereci  12067  lt2msqi  12068  le2msqi  12069  msq11i  12070  ltdiv23i  12080  fnn0ind  12628  elfzp1b  13555  elfzm1b  13556  sqrt11i  15347  sqrtmuli  15348  sqrtmsq2i  15350  sqrtlei  15351  sqrtlti  15352  fsum  15682  fprod  15906  blometi  30874  spansnm0i  31721  lnopli  32039  lnfnli  32111  opsqrlem1  32211  opsqrlem6  32216  mdslmd3i  32403  atordi  32455  mdsymlem1  32474  gsummpt2co  33109  finxpreclem4  37710  ptrecube  37941  fdc  38066  prter3  39328