Theorem mpanl1 697

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 579	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 206  df-an 396

This theorem is referenced by:  mpanl12  699  frc  5633  oeoelem  8594  ercnv  8721  frfi  9285  fin23lem23  10318  divdiv23zi  11965  recp1lt1  12110  divgt0i  12120  divge0i  12121  ltreci  12122  lereci  12123  lt2msqi  12124  le2msqi  12125  msq11i  12126  ltdiv23i  12136  fnn0ind  12659  elfzp1b  13576  elfzm1b  13577  sqrt11i  15329  sqrtmuli  15330  sqrtmsq2i  15332  sqrtlei  15333  sqrtlti  15334  fsum  15664  fprod  15883  blometi  30528  spansnm0i  31375  lnopli  31693  lnfnli  31765  opsqrlem1  31865  opsqrlem6  31870  mdslmd3i  32057  atordi  32109  mdsymlem1  32128  gsummpt2co  32671  finxpreclem4  36766  ptrecube  36982  fdc  37107  prter3  38246