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  5619  oeoelem  8638  ercnv  8770  frfi  9307  fin23lem23  10434  divdiv23zi  12100  recp1lt1  12245  divgt0i  12255  divge0i  12256  ltreci  12257  lereci  12258  lt2msqi  12259  le2msqi  12260  msq11i  12261  ltdiv23i  12271  fnn0ind  12828  elfzp1b  13765  elfzm1b  13766  sqrt11i  15584  sqrtmuli  15585  sqrtmsq2i  15587  sqrtlei  15588  sqrtlti  15589  fsum  15918  fprod  16140  blometi  31438  spansnm0i  32285  lnopli  32603  lnfnli  32675  opsqrlem1  32775  opsqrlem6  32780  mdslmd3i  32967  atordi  33019  mdsymlem1  33038  gsummpt2co  33685  jltalephlem  36038  finxpreclem4  38522  ptrecube  38743  fdc  38882  prter3  40142  grpcanonhfstruct  46241