Theorem mpanl1 700

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 580	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 207  df-an 396

This theorem is referenced by:  mpanl12  702  frc  5604  oeoelem  8565  ercnv  8695  frfi  9239  fin23lem23  10286  divdiv23zi  11942  recp1lt1  12088  divgt0i  12098  divge0i  12099  ltreci  12100  lereci  12101  lt2msqi  12102  le2msqi  12103  msq11i  12104  ltdiv23i  12114  fnn0ind  12640  elfzp1b  13569  elfzm1b  13570  sqrt11i  15358  sqrtmuli  15359  sqrtmsq2i  15361  sqrtlei  15362  sqrtlti  15363  fsum  15693  fprod  15914  blometi  30739  spansnm0i  31586  lnopli  31904  lnfnli  31976  opsqrlem1  32076  opsqrlem6  32081  mdslmd3i  32268  atordi  32320  mdsymlem1  32339  gsummpt2co  32995  finxpreclem4  37389  ptrecube  37621  fdc  37746  prter3  38882