Theorem mpancom 422

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mpan  424  spesbc  3115  onsucelsucr  4600  sucunielr  4602  ordsuc  4655  peano2b  4707  xpiindim  4859  fununfun  5364  fvelrnb  5683  fliftcnv  5925  riotaprop  5986  unielxp  6326  dmtpos  6408  tpossym  6428  ercnv  6709  cnvct  6970  php5dom  7032  3xpfi  7103  recrecnq  7589  1idpr  7787  eqlei2  8249  lem1  9002  eluzfz1  10235  fzpred  10274  uznfz  10307  fz0fzdiffz0  10334  fzctr  10337  flid  10512  flqeqceilz  10548  faclbnd3  10973  bcn1  10988  isfinite4im  11022  leabs  11593  gcd0id  12508  lcmgcdlem  12607  dvdsnprmd  12655  pcprod  12877  fldivp1  12879  intopsn  13408  mgm1  13411  sgrp1  13452  mnd1  13496  mnd1id  13497  grp1  13647  grp1inv  13648  eqger  13769  eqgid  13771  qusghm  13827  rngressid  13925  ring1  14030  ringressid  14034  subrgsubm  14206  resrhm2b  14221  lssex  14326  cncrng  14541  eltpsg  14722  tg1  14741  cldval  14781  cldss  14787  cldopn  14789  psmetdmdm  15006  dvef  15409  relogef  15546  zabsle1  15686  usgredg2vlem2  16029  wlkprop  16048  wlkvtxiedg  16066  bj-nn0suc0  16337