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  5601  oeoelem  8562  ercnv  8692  frfi  9232  fin23lem23  10279  divdiv23zi  11935  recp1lt1  12081  divgt0i  12091  divge0i  12092  ltreci  12093  lereci  12094  lt2msqi  12095  le2msqi  12096  msq11i  12097  ltdiv23i  12107  fnn0ind  12633  elfzp1b  13562  elfzm1b  13563  sqrt11i  15351  sqrtmuli  15352  sqrtmsq2i  15354  sqrtlei  15355  sqrtlti  15356  fsum  15686  fprod  15907  blometi  30732  spansnm0i  31579  lnopli  31897  lnfnli  31969  opsqrlem1  32069  opsqrlem6  32074  mdslmd3i  32261  atordi  32313  mdsymlem1  32332  gsummpt2co  32988  finxpreclem4  37382  ptrecube  37614  fdc  37739  prter3  38875