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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mpanl12  700  frc  5642  oeoelem  8597  ercnv  8723  frfi  9287  fin23lem23  10320  divdiv23zi  11966  recp1lt1  12111  divgt0i  12121  divge0i  12122  ltreci  12123  lereci  12124  lt2msqi  12125  le2msqi  12126  msq11i  12127  ltdiv23i  12137  fnn0ind  12660  elfzp1b  13577  elfzm1b  13578  sqrt11i  15330  sqrtmuli  15331  sqrtmsq2i  15333  sqrtlei  15334  sqrtlti  15335  fsum  15665  fprod  15884  blometi  30051  spansnm0i  30898  lnopli  31216  lnfnli  31288  opsqrlem1  31388  opsqrlem6  31393  mdslmd3i  31580  atordi  31632  mdsymlem1  31651  gsummpt2co  32195  finxpreclem4  36270  ptrecube  36483  fdc  36608  prter3  37747