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  5582  oeoelem  8519  ercnv  8649  frfi  9176  fin23lem23  10224  divdiv23zi  11881  recp1lt1  12027  divgt0i  12037  divge0i  12038  ltreci  12039  lereci  12040  lt2msqi  12041  le2msqi  12042  msq11i  12043  ltdiv23i  12053  fnn0ind  12578  elfzp1b  13503  elfzm1b  13504  sqrt11i  15294  sqrtmuli  15295  sqrtmsq2i  15297  sqrtlei  15298  sqrtlti  15299  fsum  15629  fprod  15850  blometi  30785  spansnm0i  31632  lnopli  31950  lnfnli  32022  opsqrlem1  32122  opsqrlem6  32127  mdslmd3i  32314  atordi  32366  mdsymlem1  32385  gsummpt2co  33035  finxpreclem4  37459  ptrecube  37680  fdc  37805  prter3  39001