Theorem mpanl1 713

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanl12  715  frc  5613  oeoelem  8610  ercnv  8742  frfi  9279  fin23lem23  10407  divdiv23zi  12073  recp1lt1  12218  divgt0i  12228  divge0i  12229  ltreci  12230  lereci  12231  lt2msqi  12232  le2msqi  12233  msq11i  12234  ltdiv23i  12244  fnn0ind  12801  elfzp1b  13738  elfzm1b  13739  sqrt11i  15557  sqrtmuli  15558  sqrtmsq2i  15560  sqrtlei  15561  sqrtlti  15562  fsum  15891  fprod  16113  blometi  31410  spansnm0i  32257  lnopli  32575  lnfnli  32647  opsqrlem1  32747  opsqrlem6  32752  mdslmd3i  32939  atordi  32991  mdsymlem1  33010  gsummpt2co  33655  finxpreclem4  38410  ptrecube  38631  fdc  38772  prter3  40032