Theorem mpanl1 699

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  mpanl12  701  frc  5485  oeoelem  8207  ercnv  8293  frfi  8747  fin23lem23  9737  divdiv23zi  11382  recp1lt1  11527  divgt0i  11537  divge0i  11538  ltreci  11539  lereci  11540  lt2msqi  11541  le2msqi  11542  msq11i  11543  ltdiv23i  11553  fnn0ind  12069  elfzp1b  12979  elfzm1b  12980  sqrt11i  14736  sqrtmuli  14737  sqrtmsq2i  14739  sqrtlei  14740  sqrtlti  14741  fsum  15069  fprod  15287  blometi  28586  spansnm0i  29433  lnopli  29751  lnfnli  29823  opsqrlem1  29923  opsqrlem6  29928  mdslmd3i  30115  atordi  30167  mdsymlem1  30186  gsummpt2co  30733  finxpreclem4  34811  ptrecube  35057  fdc  35183  prter3  36178