Theorem mpancom 426

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mpan  428  spesbc  3138  onsucelsucr  4657  sucunielr  4659  ordsuc  4712  peano2b  4764  xpiindim  4919  fununfun  5427  fvelrnb  5753  fliftcnv  6004  riotaprop  6067  unielxp  6412  dmtpos  6532  tpossym  6552  ercnv  6833  cnvct  7103  php5dom  7170  3xpfi  7247  recrecnq  7768  1idpr  7966  eqlei2  8428  lem1  9186  eluzfz1  10452  fzpred  10494  uznfz  10527  fz0fzdiffz0  10554  fzctr  10557  flid  10740  flqeqceilz  10776  faclbnd3  11203  bcn1  11218  isfinite4im  11253  hashfac  11310  leabs  11862  gcd0id  12781  lcmgcdlem  12880  dvdsnprmd  12928  pcprod  13154  fldivp1  13156  intopsn  13746  mgm1  13749  sgrp1  13785  mnd1  13821  mnd1id  13822  grp1  13970  grp1inv  13971  eqger  14086  eqgid  14088  qusghm  14144  cntzrcl  14159  rngressid  14360  ring1  14471  ringressid  14477  subrgsubm  14651  resrhm2b  14666  lssex  14800  cncrng  15015  ressascl  15148  psrbaglesupp  15172  eltpsg  15299  tg1  15318  cldval  15358  cldss  15364  cldopn  15366  psmetdmdm  15583  dvef  15986  relogef  16126  bposlem7  16350  zabsle1  16356  usgredg2vlem2  16702  wlkprop  16806  wlkvtxiedg  16824  eupthseg  16931  bj-nn0suc0  17214