Theorem mpanl1 710

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  mpanl12  712  frc  5608  oeoelem  8563  ercnv  8695  frfi  9225  fin23lem23  10280  divdiv23zi  11941  recp1lt1  12087  divgt0i  12097  divge0i  12098  ltreci  12099  lereci  12100  lt2msqi  12101  le2msqi  12102  msq11i  12103  ltdiv23i  12113  fnn0ind  12669  elfzp1b  13603  elfzm1b  13604  sqrt11i  15395  sqrtmuli  15396  sqrtmsq2i  15398  sqrtlei  15399  sqrtlti  15400  fsum  15730  fprod  15954  blometi  30952  spansnm0i  31799  lnopli  32117  lnfnli  32189  opsqrlem1  32289  opsqrlem6  32294  mdslmd3i  32481  atordi  32533  mdsymlem1  32552  gsummpt2co  33189  finxpreclem4  37852  ptrecube  38083  fdc  38208  prter3  39470