Theorem mpancom 413

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 403	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mpan  415  spesbc  2913  onsucelsucr  4298  sucunielr  4300  ordsuc  4352  peano2b  4402  xpiindim  4541  fvelrnb  5315  fliftcnv  5535  riotaprop  5592  unielxp  5901  dmtpos  5975  tpossym  5995  ercnv  6265  cnvct  6478  php5dom  6531  3xpfi  6591  recrecnq  6897  1idpr  7095  eqlei2  7523  lem1  8243  eluzfz1  9377  fzpred  9414  uznfz  9447  fz0fzdiffz0  9469  fzctr  9472  flid  9619  flqeqceilz  9653  faclbnd3  10047  bcn1  10062  isfinite4im  10097  leabs  10402  gcd0id  10845  lcmgcdlem  10934  dvdsnprmd  10982  bj-nn0suc0  11283