Theorem mpanl1 701

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 581	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  703  frc  5595  oeoelem  8536  ercnv  8667  frfi  9197  fin23lem23  10248  divdiv23zi  11906  recp1lt1  12052  divgt0i  12062  divge0i  12063  ltreci  12064  lereci  12065  lt2msqi  12066  le2msqi  12067  msq11i  12068  ltdiv23i  12078  fnn0ind  12603  elfzp1b  13529  elfzm1b  13530  sqrt11i  15320  sqrtmuli  15321  sqrtmsq2i  15323  sqrtlei  15324  sqrtlti  15325  fsum  15655  fprod  15876  blometi  30890  spansnm0i  31737  lnopli  32055  lnfnli  32127  opsqrlem1  32227  opsqrlem6  32232  mdslmd3i  32419  atordi  32471  mdsymlem1  32490  gsummpt2co  33141  finxpreclem4  37643  ptrecube  37865  fdc  37990  prter3  39252