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  5617  oeoelem  8610  ercnv  8740  frfi  9293  fin23lem23  10340  divdiv23zi  11994  recp1lt1  12140  divgt0i  12150  divge0i  12151  ltreci  12152  lereci  12153  lt2msqi  12154  le2msqi  12155  msq11i  12156  ltdiv23i  12166  fnn0ind  12692  elfzp1b  13618  elfzm1b  13619  sqrt11i  15403  sqrtmuli  15404  sqrtmsq2i  15406  sqrtlei  15407  sqrtlti  15408  fsum  15736  fprod  15957  blometi  30784  spansnm0i  31631  lnopli  31949  lnfnli  32021  opsqrlem1  32121  opsqrlem6  32126  mdslmd3i  32313  atordi  32365  mdsymlem1  32384  gsummpt2co  33042  finxpreclem4  37412  ptrecube  37644  fdc  37769  prter3  38900