Theorem mpanl1 708

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 530	. 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓))
3		mpanl1.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 588	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  710  frc  5603  oeoelem  8556  ercnv  8688  frfi  9218  fin23lem23  10273  divdiv23zi  11934  recp1lt1  12080  divgt0i  12090  divge0i  12091  ltreci  12092  lereci  12093  lt2msqi  12094  le2msqi  12095  msq11i  12096  ltdiv23i  12106  fnn0ind  12662  elfzp1b  13596  elfzm1b  13597  sqrt11i  15388  sqrtmuli  15389  sqrtmsq2i  15391  sqrtlei  15392  sqrtlti  15393  fsum  15723  fprod  15947  blometi  30945  spansnm0i  31792  lnopli  32110  lnfnli  32182  opsqrlem1  32282  opsqrlem6  32287  mdslmd3i  32474  atordi  32526  mdsymlem1  32545  gsummpt2co  33182  finxpreclem4  37836  ptrecube  38067  fdc  38192  prter3  39454