Theorem mpanl2 701

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 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:  mpanr1  703  mp3an2  1451  reuss  4280  tfrlem11  8317  tfr3  8328  oe0  8447  unfi  9095  dif1ennnALT  9180  indpi  10820  map2psrpr  11023  axcnre  11077  muleqadd  11782  divdiv2  11854  addltmul  12378  supxrpnf  13238  supxrunb1  13239  supxrunb2  13240  iimulcl  24849  clwwlknonex2lem2  30070  nmopadjlem  32051  nmopcoadji  32063  opsqrlem6  32107  hstrbi  32228  sgncl  32789  poimirlem3  37602  dflim5  43302  aacllem  49787