Theorem mpanl1 696

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 206  df-an 396

This theorem is referenced by:  mpanl12  698  frc  5546  oeoelem  8391  ercnv  8477  frfi  8989  fin23lem23  10013  divdiv23zi  11658  recp1lt1  11803  divgt0i  11813  divge0i  11814  ltreci  11815  lereci  11816  lt2msqi  11817  le2msqi  11818  msq11i  11819  ltdiv23i  11829  fnn0ind  12349  elfzp1b  13262  elfzm1b  13263  sqrt11i  15024  sqrtmuli  15025  sqrtmsq2i  15027  sqrtlei  15028  sqrtlti  15029  fsum  15360  fprod  15579  blometi  29066  spansnm0i  29913  lnopli  30231  lnfnli  30303  opsqrlem1  30403  opsqrlem6  30408  mdslmd3i  30595  atordi  30647  mdsymlem1  30666  gsummpt2co  31210  finxpreclem4  35492  ptrecube  35704  fdc  35830  prter3  36823