Theorem mpancom 399

Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)

Hypotheses

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

Assertion

Ref	Expression
mpancom	⊢ (𝜓 → 𝜒)

Proof of Theorem mpancom

Step	Hyp	Ref	Expression
1		mpancom.1	. 2 ⊢ (𝜓 → 𝜑)
2		id 19	. 2 ⊢ (𝜓 → 𝜓)
3		mpancom.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 391	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 101

This theorem is referenced by:  mpan  400  spesbc  2843  onsucelsucr  4234  sucunielr  4236  ordsuc  4287  peano2b  4337  xpiindim  4473  fvelrnb  5221  fliftcnv  5435  riotaprop  5491  unielxp  5800  dmtpos  5871  tpossym  5891  ercnv  6127  php5dom  6325  recrecnq  6492  1idpr  6690  eqlei2  7112  lem1  7813  eluzfz1  8895  fzpred  8932  uznfz  8965  fz0fzdiffz0  8987  fzctr  8991  flid  9126  flqeqceilz  9160  leabs  9672  bj-nn0suc0  10075