Theorem mpanl1 712

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 532	. 2 ⊢ (𝜓 → (𝜑 ∧ 𝜓))
3		mpanl1.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 591	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpanl12  714  frc  5615  oeoelem  8572  ercnv  8704  frfi  9233  fin23lem23  10298  divdiv23zi  11959  recp1lt1  12104  divgt0i  12114  divge0i  12115  ltreci  12116  lereci  12117  lt2msqi  12118  le2msqi  12119  msq11i  12120  ltdiv23i  12130  fnn0ind  12686  elfzp1b  13620  elfzm1b  13621  sqrt11i  15426  sqrtmuli  15427  sqrtmsq2i  15429  sqrtlei  15430  sqrtlti  15431  fsum  15761  fprod  15985  blometi  31064  spansnm0i  31911  lnopli  32229  lnfnli  32301  opsqrlem1  32401  opsqrlem6  32406  mdslmd3i  32593  atordi  32645  mdsymlem1  32664  gsummpt2co  33281  finxpreclem4  37900  ptrecube  38131  fdc  38256  prter3  39518