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  5614  oeoelem  8591  ercnv  8723  frfi  9260  fin23lem23  10385  divdiv23zi  12051  recp1lt1  12196  divgt0i  12206  divge0i  12207  ltreci  12208  lereci  12209  lt2msqi  12210  le2msqi  12211  msq11i  12212  ltdiv23i  12222  fnn0ind  12779  elfzp1b  13715  elfzm1b  13716  sqrt11i  15532  sqrtmuli  15533  sqrtmsq2i  15535  sqrtlei  15536  sqrtlti  15537  fsum  15866  fprod  16088  blometi  31387  spansnm0i  32234  lnopli  32552  lnfnli  32624  opsqrlem1  32724  opsqrlem6  32729  mdslmd3i  32916  atordi  32968  mdsymlem1  32987  gsummpt2co  33591  finxpreclem4  38285  ptrecube  38506  fdc  38647  prter3  39907