Theorem mpancom 686

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpan  688  spesbc  3865  csbie2df  4392  xpiindi  5706  fununfun  6402  dffv2  6756  fliftcnv  7064  riotaprop  7141  elovmpt3rab1  7405  3xpexg  7475  orduniorsuc  7545  unielxp  7727  dmtpos  7904  tpossym  7924  wfrlem5  7959  oesuclem  8150  ercnv  8310  cnvct  8586  undom  8605  sucxpdom  8727  3xpfi  8790  pwfilem  8818  rankr1id  9291  cardnn  9392  alephnbtwn2  9498  alephsucdom  9505  cdainflem  9613  isfin4p1  9737  axcclem  9879  dmct  9946  mptct  9960  infxpidm  9984  fpwwe2lem9  10060  gchpwdom  10092  elwina  10108  elina  10109  rankcf  10199  ltexprlem4  10461  lem1  11483  ltdivp1i  11566  rpnnen1lem5  12381  eluzfz1  12915  fzpred  12956  uznfz  12991  fz0fzdiffz0  13017  fzctr  13020  flid  13179  modid0  13266  2txmodxeq0  13300  faclbnd3  13653  faclbnd4lem4  13657  bcn1  13674  hashfac  13817  repswsymballbi  14142  wrdlen2i  14304  dfrtrclrec2  14416  rtrclreclem3  14419  rtrclreclem4  14420  relexpindlem  14422  sqrtsq  14629  absrdbnd  14701  sqreulem  14719  sqreu  14720  bpoly2  15411  bpoly3  15412  gcd0id  15867  lcmgcdlem  15950  lcmftp  15980  dvdsnprmd  16034  2mulprm  16037  pcprod  16231  fldivp1  16233  invsym2  17033  pleval2i  17574  smndlsmidm  18781  subrgsubm  19548  cncrng  20566  znchr  20709  mattposvs  21064  smadiadetglem2  21281  tg1  21572  cldval  21631  cldss  21637  cldopn  21639  1stcrestlem  22060  refbas  22118  refssex  22119  regr1  22358  kqreg  22359  kqnrm  22360  ufilen  22538  efmndtmd  22709  symgtgp  22714  elrnust  22833  psmetdmdm  22915  metuval  23159  icoopnst  23543  cnheiborlem  23558  cfilfcls  23877  eflogeq  25185  logdivlt  25204  logdifbnd  25571  harmonicbnd4  25588  basellem5  25662  bposlem7  25866  zabsle1  25872  addsqn2reu  26017  chto1ub  26052  chpo1ub  26056  vmadivsum  26058  dchrmusum2  26070  dchrvmasum2if  26073  dchrvmasumlema  26076  dchrvmasumiflem2  26078  dchrisum0re  26089  dchrvmasumlem  26099  rplogsum  26103  mulogsumlem  26107  logdivsum  26109  selberg2lem  26126  pntrmax  26140  pntlem3  26185  pntleml  26187  pnt2  26189  usgredg2vlem2  27008  vtxdgelxnn0  27254  wlkonprop  27440  wksonproplem  27486  wwlknbp  27620  wspthnp  27628  wlklnwwlkln1  27646  clwwlkf  27826  erclwwlknsym  27849  erclwwlkntr  27850  eupth0  27993  numclwwlk1lem2fo  28137  numclwlk2lem2f  28156  numclwwlk5lem  28166  hilablo  28937  hhssabloilem  29038  mayete3i  29505  homulid2  29577  adjeu  29666  lnopeqi  29785  cnlnadjlem7  29850  adjbdlnb  29861  nmopcoadji  29878  bracnlnval  29891  elunirn2  30396  mptctf  30453  xraddge02  30480  xrge0npcan  30681  gsumle  30725  gsumvsca1  30854  gsumvsca2  30855  metidval  31130  pstmval  31135  baselsiga  31374  sigasspw  31375  ddeval1  31493  ddeval0  31494  braew  31501  derangen2  32421  subfaclim  32435  snmlff  32576  elfzm12  32918  noextendlt  33176  fnetr  33699  wl-sbal1  34814  poimirlem13  34920  poimirlem14  34921  poimirlem31  34938  poimirlem32  34939  ismblfin  34948  itg2addnclem2  34959  areacirclem2  34998  areacirc  35002  ismgmOLD  35143  ismndo2  35167  rngomndo  35228  cnvepimaex  35608  dmqseq  35890  prter3  36033  atbase  36440  llnbase  36660  lplnbase  36685  lvolbase  36729  lhpbase  37149  rernegcl  39221  renegadd  39222  reneg0addid2  39224  sn-0ne2  39256  3cubes  39307  mzpsubmpt  39360  mzpnegmpt  39361  eliunov2  40044  iunrelexp0  40067  enmappwid  40366  uunT1  41134  nnfoctb  41329  afveu  43372  afv2eu  43457  afv20fv0  43482  fzopredsuc  43543  fargshiftfva  43623  lindsrng01  44543