Theorem mpanl1 700

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 580	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 207  df-an 396

This theorem is referenced by:  mpanl12  702  frc  5648  oeoelem  8636  ercnv  8766  frfi  9321  fin23lem23  10366  divdiv23zi  12020  recp1lt1  12166  divgt0i  12176  divge0i  12177  ltreci  12178  lereci  12179  lt2msqi  12180  le2msqi  12181  msq11i  12182  ltdiv23i  12192  fnn0ind  12717  elfzp1b  13641  elfzm1b  13642  sqrt11i  15423  sqrtmuli  15424  sqrtmsq2i  15426  sqrtlei  15427  sqrtlti  15428  fsum  15756  fprod  15977  blometi  30822  spansnm0i  31669  lnopli  31987  lnfnli  32059  opsqrlem1  32159  opsqrlem6  32164  mdslmd3i  32351  atordi  32403  mdsymlem1  32422  gsummpt2co  33051  finxpreclem4  37395  ptrecube  37627  fdc  37752  prter3  38883