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  5652  oeoelem  8635  ercnv  8765  frfi  9319  fin23lem23  10364  divdiv23zi  12018  recp1lt1  12164  divgt0i  12174  divge0i  12175  ltreci  12176  lereci  12177  lt2msqi  12178  le2msqi  12179  msq11i  12180  ltdiv23i  12190  fnn0ind  12715  elfzp1b  13638  elfzm1b  13639  sqrt11i  15420  sqrtmuli  15421  sqrtmsq2i  15423  sqrtlei  15424  sqrtlti  15425  fsum  15753  fprod  15974  blometi  30832  spansnm0i  31679  lnopli  31997  lnfnli  32069  opsqrlem1  32169  opsqrlem6  32174  mdslmd3i  32361  atordi  32413  mdsymlem1  32432  gsummpt2co  33034  finxpreclem4  37377  ptrecube  37607  fdc  37732  prter3  38864