Theorem mpancom 694

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 22	. 2 ⊢ (𝜓 → 𝜓)
3		mpancom.2	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
4	1, 2, 3	syl2anc 590	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 208  df-an 397

This theorem is referenced by:  mpan  696  spesbc  3821  csbie2df  4378  xpiindi  5784  fununfun  6540  dffv2  6929  fliftcnv  7262  riotaprop  7347  elovmpt3rab1  7623  3xpexg  7702  orduniorsuc  7777  unielxp  7976  dmtpos  8185  tpossym  8205  oesuclem  8457  ercnv  8662  cnvct  8978  sucxpdom  9168  enp1i  9186  pwfilem  9225  3xpfi  9228  rankr1id  9784  cardnn  9885  alephnbtwn2  9992  alephsucdom  9999  cdainflem  10108  isfin4p1  10235  axcclem  10377  dmct  10444  mptct  10458  infxpidm  10482  fpwwe2lem8  10559  gchpwdom  10591  elwina  10607  elina  10608  rankcf  10698  ltexprlem4  10960  lem1  11996  ltdivp1i  12080  nn0le2x  12489  rpnnen1lem5  12929  eluzfz1  13483  fzpred  13524  uznfz  13562  fz0fzdiffz0  13589  fzctr  13592  flid  13765  modid0  13854  2txmodxeq0  13891  faclbnd3  14252  faclbnd4lem4  14256  bcn1  14273  hashfac  14418  repswsymballbi  14740  wrdlen2i  14902  dfrtrclrec2  15018  rtrclreclem3  15020  rtrclreclem4  15021  relexpindlem  15023  sqrtsq  15229  absrdbnd  15302  sqreulem  15320  sqreu  15321  bpoly2  16020  bpoly3  16021  gcd0id  16486  lcmgcdlem  16573  lcmftp  16603  dvdsnprmd  16657  2mulprm  16660  pcprod  16864  fldivp1  16866  invsym2  17728  pleval2i  18298  smndlsmidm  19629  gsumle  20118  subrgsubm  20564  resrhm2b  20581  pzriprnglem11  21473  znchr  21544  psrbagfsupp  21901  mattposvs  22445  smadiadetglem2  22662  tg1  22954  cldval  23013  cldss  23019  cldopn  23021  1stcrestlem  23442  refbas  23500  refssex  23501  regr1  23740  kqreg  23741  kqnrm  23742  ufilen  23920  efmndtmd  24091  symgtgp  24096  psmetdmdm  24295  icoopnst  24931  cnheiborlem  24946  cfilfcls  25266  eflogeq  26591  logdivlt  26610  logdifbnd  26982  harmonicbnd4  26999  basellem5  27073  bposlem7  27278  zabsle1  27284  addsqn2reu  27429  chto1ub  27464  chpo1ub  27468  vmadivsum  27470  dchrmusum2  27482  dchrvmasum2if  27485  dchrvmasumlema  27488  dchrvmasumiflem2  27490  dchrisum0re  27501  dchrvmasumlem  27511  rplogsum  27515  mulogsumlem  27519  logdivsum  27521  selberg2lem  27538  pntrmax  27552  pntlem3  27597  pntleml  27599  pnt2  27601  noextendlt  27658  usgredg2vlem2  29320  vtxdgelxnn0  29566  wlkonprop  29750  wksonproplem  29796  wwlknbp  29935  wspthnp  29943  wlklnwwlkln1  29961  clwwlkf  30142  erclwwlknsym  30165  erclwwlkntr  30166  eupth0  30309  numclwwlk1lem2fo  30453  numclwlk2lem2f  30472  numclwwlk5lem  30482  hilablo  31256  hhssabloilem  31357  mayete3i  31824  homullid  31896  adjeu  31985  lnopeqi  32104  cnlnadjlem7  32169  adjbdlnb  32180  nmopcoadji  32197  bracnlnval  32210  mptctf  32815  xraddge02  32856  xrge0npcan  33106  gsumvsca1  33314  gsumvsca2  33315  baselsiga  34306  sigasspw  34307  ddeval1  34425  ddeval0  34426  braew  34433  derangen2  35409  subfaclim  35423  snmlff  35564  elfzm12  35910  fnetr  36586  wl-sbal1  37941  poimirlem13  38007  poimirlem14  38008  poimirlem31  38025  poimirlem32  38026  ismblfin  38035  itg2addnclem2  38046  areacirclem2  38083  areacirc  38087  ismgmOLD  38224  ismndo2  38248  rngomndo  38309  ecxrn2  38782  dmqseq  39098  prter3  39381  atbase  39788  llnbase  40008  lplnbase  40033  lvolbase  40077  lhpbase  40497  rernegcl  42855  renegadd  42856  reneg0addlid  42858  sn-0ne2  42890  3cubes  43146  mzpsubmpt  43199  mzpnegmpt  43200  eliunov2  44130  iunrelexp0  44153  enmappwid  44451  uunT1  45230  nnfoctb  45503  rn1st  45724  afveu  47623  afv2eu  47708  afv20fv0  47733  fzopredsuc  47794  fargshiftfva  47925  lindsrng01  48966  cic1st2nd  49544  cicpropdlem  49546  zeroo2  49731