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  5587  oeoelem  8526  ercnv  8656  frfi  9185  fin23lem23  10236  divdiv23zi  11894  recp1lt1  12040  divgt0i  12050  divge0i  12051  ltreci  12052  lereci  12053  lt2msqi  12054  le2msqi  12055  msq11i  12056  ltdiv23i  12066  fnn0ind  12591  elfzp1b  13517  elfzm1b  13518  sqrt11i  15308  sqrtmuli  15309  sqrtmsq2i  15311  sqrtlei  15312  sqrtlti  15313  fsum  15643  fprod  15864  blometi  30878  spansnm0i  31725  lnopli  32043  lnfnli  32115  opsqrlem1  32215  opsqrlem6  32220  mdslmd3i  32407  atordi  32459  mdsymlem1  32478  gsummpt2co  33131  finxpreclem4  37595  ptrecube  37817  fdc  37942  prter3  39138