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  5622  oeoelem  8590  ercnv  8722  frfi  9259  fin23lem23  10332  divdiv23zi  11996  recp1lt1  12141  divgt0i  12151  divge0i  12152  ltreci  12153  lereci  12154  lt2msqi  12155  le2msqi  12156  msq11i  12157  ltdiv23i  12167  fnn0ind  12724  elfzp1b  13660  elfzm1b  13661  sqrt11i  15476  sqrtmuli  15477  sqrtmsq2i  15479  sqrtlei  15480  sqrtlti  15481  fsum  15810  fprod  16034  blometi  31292  spansnm0i  32139  lnopli  32457  lnfnli  32529  opsqrlem1  32629  opsqrlem6  32634  mdslmd3i  32821  atordi  32873  mdsymlem1  32892  gsummpt2co  33496  finxpreclem4  38156  ptrecube  38377  fdc  38503  prter3  39763