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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  mpanl12  699  frc  5555  oeoelem  8429  ercnv  8519  frfi  9059  fin23lem23  10082  divdiv23zi  11728  recp1lt1  11873  divgt0i  11883  divge0i  11884  ltreci  11885  lereci  11886  lt2msqi  11887  le2msqi  11888  msq11i  11889  ltdiv23i  11899  fnn0ind  12419  elfzp1b  13333  elfzm1b  13334  sqrt11i  15096  sqrtmuli  15097  sqrtmsq2i  15099  sqrtlei  15100  sqrtlti  15101  fsum  15432  fprod  15651  blometi  29165  spansnm0i  30012  lnopli  30330  lnfnli  30402  opsqrlem1  30502  opsqrlem6  30507  mdslmd3i  30694  atordi  30746  mdsymlem1  30765  gsummpt2co  31308  finxpreclem4  35565  ptrecube  35777  fdc  35903  prter3  36896