Theorem mpanl1 696

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 522	. 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓))
3		mpanl1.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 578	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  mpanl12  698  frc  5641  oeoelem  8600  ercnv  8726  frfi  9290  fin23lem23  10323  divdiv23zi  11971  recp1lt1  12116  divgt0i  12126  divge0i  12127  ltreci  12128  lereci  12129  lt2msqi  12130  le2msqi  12131  msq11i  12132  ltdiv23i  12142  fnn0ind  12665  elfzp1b  13582  elfzm1b  13583  sqrt11i  15335  sqrtmuli  15336  sqrtmsq2i  15338  sqrtlei  15339  sqrtlti  15340  fsum  15670  fprod  15889  blometi  30323  spansnm0i  31170  lnopli  31488  lnfnli  31560  opsqrlem1  31660  opsqrlem6  31665  mdslmd3i  31852  atordi  31904  mdsymlem1  31923  gsummpt2co  32470  finxpreclem4  36578  ptrecube  36791  fdc  36916  prter3  38055