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  4272  tfrlem11  8399  tfr3  8410  oe0  8533  unfi  9189  dif1ennnALT  9271  indpi  10995  map2psrpr  11198  axcnre  11252  muleqadd  11963  divdiv2  12032  addltmul  12585  supxrpnf  13451  supxrunb1  13452  supxrunb2  13453  sgncl  15255  iimulcl  25263  clwwlknonex2lem2  30704  nmopadjlem  32696  nmopcoadji  32708  opsqrlem6  32752  hstrbi  32873  poimirlem3  38634  dflim5  44424  aacllem  51107