Theorem mpanl1 688

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  mpanl12  690  frc  5369  oeoelem  8023  ercnv  8108  frfi  8556  fin23lem23  9544  divdiv23zi  11192  recp1lt1  11337  divgt0i  11347  divge0i  11348  ltreci  11349  lereci  11350  lt2msqi  11351  le2msqi  11352  msq11i  11353  ltdiv23i  11363  fnn0ind  11892  elfzp1b  12798  elfzm1b  12799  sqrt11i  14603  sqrtmuli  14604  sqrtmsq2i  14606  sqrtlei  14607  sqrtlti  14608  fsum  14935  fprod  15153  blometi  28372  spansnm0i  29223  lnopli  29541  lnfnli  29613  opsqrlem1  29713  opsqrlem6  29718  mdslmd3i  29905  atordi  29957  mdsymlem1  29976  gsummpt2co  30555  finxpreclem4  34153  ptrecube  34370  fdc  34499  prter3  35500