Theorem mpanl1 699

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 579	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  701  frc  5663  oeoelem  8654  ercnv  8784  frfi  9349  fin23lem23  10395  divdiv23zi  12047  recp1lt1  12193  divgt0i  12203  divge0i  12204  ltreci  12205  lereci  12206  lt2msqi  12207  le2msqi  12208  msq11i  12209  ltdiv23i  12219  fnn0ind  12742  elfzp1b  13661  elfzm1b  13662  sqrt11i  15433  sqrtmuli  15434  sqrtmsq2i  15436  sqrtlei  15437  sqrtlti  15438  fsum  15768  fprod  15989  blometi  30835  spansnm0i  31682  lnopli  32000  lnfnli  32072  opsqrlem1  32172  opsqrlem6  32177  mdslmd3i  32364  atordi  32416  mdsymlem1  32435  gsummpt2co  33031  finxpreclem4  37360  ptrecube  37580  fdc  37705  prter3  38838