Theorem mpanl1 713

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

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

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 402

This theorem is used by:  mpanl12  715  frc  5629  oeoelem  8593  ercnv  8725  frfi  9255  fin23lem23  10328  divdiv23zi  11986  recp1lt1  12131  divgt0i  12141  divge0i  12142  ltreci  12143  lereci  12144  lt2msqi  12145  le2msqi  12146  msq11i  12147  ltdiv23i  12157  fnn0ind  12713  elfzp1b  13648  elfzm1b  13649  sqrt11i  15462  sqrtmuli  15463  sqrtmsq2i  15465  sqrtlei  15466  sqrtlti  15467  fsum  15797  fprod  16021  blometi  31192  spansnm0i  32039  lnopli  32357  lnfnli  32429  opsqrlem1  32529  opsqrlem6  32534  mdslmd3i  32721  atordi  32773  mdsymlem1  32792  gsummpt2co  33399  finxpreclem4  38081  ptrecube  38312  fdc  38437  prter3  39697