Theorem mpanl2 697

Description: An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpanl2.1	⊢ 𝜓
mpanl2.2	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mpanl2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpanl2

Step	Hyp	Ref	Expression
1		mpanl2.1	. . 3 ⊢ 𝜓
2	1	jctr 524	. 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓))
3		mpanl2.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 579	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 206  df-an 396

This theorem is referenced by:  mpanr1  699  mp3an2  1447  reuss  4247  tfrlem11  8190  tfr3  8201  oe0  8314  unfi  8917  dif1enALT  8980  indpi  10594  map2psrpr  10797  axcnre  10851  muleqadd  11549  divdiv2  11617  addltmul  12139  supxrpnf  12981  supxrunb1  12982  supxrunb2  12983  iimulcl  24006  clwwlknonex2lem2  28373  nmopadjlem  30352  nmopcoadji  30364  opsqrlem6  30408  hstrbi  30529  sgncl  32405  poimirlem3  35707  aacllem  46391