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  5579  oeoelem  8513  ercnv  8643  frfi  9169  fin23lem23  10214  divdiv23zi  11871  recp1lt1  12017  divgt0i  12027  divge0i  12028  ltreci  12029  lereci  12030  lt2msqi  12031  le2msqi  12032  msq11i  12033  ltdiv23i  12043  fnn0ind  12569  elfzp1b  13498  elfzm1b  13499  sqrt11i  15289  sqrtmuli  15290  sqrtmsq2i  15292  sqrtlei  15293  sqrtlti  15294  fsum  15624  fprod  15845  blometi  30778  spansnm0i  31625  lnopli  31943  lnfnli  32015  opsqrlem1  32115  opsqrlem6  32120  mdslmd3i  32307  atordi  32359  mdsymlem1  32378  gsummpt2co  33023  finxpreclem4  37427  ptrecube  37659  fdc  37784  prter3  38920