Theorem mpanl1 698

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpanl12  700  frc  5515  oeoelem  8218  ercnv  8304  frfi  8757  fin23lem23  9742  divdiv23zi  11387  recp1lt1  11532  divgt0i  11542  divge0i  11543  ltreci  11544  lereci  11545  lt2msqi  11546  le2msqi  11547  msq11i  11548  ltdiv23i  11558  fnn0ind  12075  elfzp1b  12978  elfzm1b  12979  sqrt11i  14738  sqrtmuli  14739  sqrtmsq2i  14741  sqrtlei  14742  sqrtlti  14743  fsum  15071  fprod  15289  blometi  28574  spansnm0i  29421  lnopli  29739  lnfnli  29811  opsqrlem1  29911  opsqrlem6  29916  mdslmd3i  30103  atordi  30155  mdsymlem1  30174  gsummpt2co  30681  finxpreclem4  34669  ptrecube  34886  fdc  35014  prter3  36012