Theorem mpanl2 714

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 534	. 2 ⊢ (𝜑 → (𝜑 ∧ 𝜓))
3		mpanl2.2	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	2, 3	sylan 592	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpanr1  716  mp3an2  1478  reuss  4283  tfrlem11  8384  tfr3  8395  oe0  8516  unfi  9165  dif1ennnALT  9247  indpi  10910  map2psrpr  11113  axcnre  11167  muleqadd  11876  divdiv2  11945  addltmul  12498  supxrpnf  13362  supxrunb1  13363  supxrunb2  13364  sgncl  15160  iimulcl  25133  clwwlknonex2lem2  30496  nmopadjlem  32478  nmopcoadji  32490  opsqrlem6  32534  hstrbi  32655  poimirlem3  38315  dflim5  44097  aacllem  50662