Theorem mpanl1 701

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 581	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  703  frc  5587  oeoelem  8527  ercnv  8658  frfi  9188  fin23lem23  10239  divdiv23zi  11899  recp1lt1  12045  divgt0i  12055  divge0i  12056  ltreci  12057  lereci  12058  lt2msqi  12059  le2msqi  12060  msq11i  12061  ltdiv23i  12071  fnn0ind  12619  elfzp1b  13546  elfzm1b  13547  sqrt11i  15338  sqrtmuli  15339  sqrtmsq2i  15341  sqrtlei  15342  sqrtlti  15343  fsum  15673  fprod  15897  blometi  30889  spansnm0i  31736  lnopli  32054  lnfnli  32126  opsqrlem1  32226  opsqrlem6  32231  mdslmd3i  32418  atordi  32470  mdsymlem1  32489  gsummpt2co  33124  finxpreclem4  37724  ptrecube  37955  fdc  38080  prter3  39342