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  5586  oeoelem  8523  ercnv  8653  frfi  9190  fin23lem23  10239  divdiv23zi  11895  recp1lt1  12041  divgt0i  12051  divge0i  12052  ltreci  12053  lereci  12054  lt2msqi  12055  le2msqi  12056  msq11i  12057  ltdiv23i  12067  fnn0ind  12593  elfzp1b  13522  elfzm1b  13523  sqrt11i  15310  sqrtmuli  15311  sqrtmsq2i  15313  sqrtlei  15314  sqrtlti  15315  fsum  15645  fprod  15866  blometi  30765  spansnm0i  31612  lnopli  31930  lnfnli  32002  opsqrlem1  32102  opsqrlem6  32107  mdslmd3i  32294  atordi  32346  mdsymlem1  32365  gsummpt2co  33014  finxpreclem4  37367  ptrecube  37599  fdc  37724  prter3  38860