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  5626  oeoelem  8585  ercnv  8717  frfi  9246  fin23lem23  10311  divdiv23zi  11969  recp1lt1  12114  divgt0i  12124  divge0i  12125  ltreci  12126  lereci  12127  lt2msqi  12128  le2msqi  12129  msq11i  12130  ltdiv23i  12140  fnn0ind  12696  elfzp1b  13631  elfzm1b  13632  sqrt11i  15438  sqrtmuli  15439  sqrtmsq2i  15441  sqrtlei  15442  sqrtlti  15443  fsum  15773  fprod  15997  blometi  31133  spansnm0i  31980  lnopli  32298  lnfnli  32370  opsqrlem1  32470  opsqrlem6  32475  mdslmd3i  32662  atordi  32714  mdsymlem1  32733  gsummpt2co  33346  finxpreclem4  38018  ptrecube  38249  fdc  38374  prter3  39634