Theorem mpanl1 712

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  mpanl12  714  frc  5004  oeoelem  7565  ercnv  7650  frfi  8090  fin23lem23  9031  divdiv23zi  10657  recp1lt1  10800  divgt0i  10811  divge0i  10812  ltreci  10813  lereci  10814  lt2msqi  10815  le2msqi  10816  msq11i  10817  ltdiv23i  10827  fnn0ind  11352  elfzp1b  12286  elfzm1b  12287  sqrt11i  13972  sqrtmuli  13973  sqrtmsq2i  13975  sqrtlei  13976  sqrtlti  13977  fsum  14298  fprod  14510  blometi  27042  spansnm0i  27893  lnopli  28211  lnfnli  28283  opsqrlem1  28383  opsqrlem6  28388  mdslmd3i  28575  atordi  28627  mdsymlem1  28646  gsummpt2co  29111  finxpreclem4  32407  ptrecube  32579  fdc  32711  prter3  33185