Theorem mpancom 700

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  mpan  702  spesbc  3838  csbie2df  4400  xpiindi  5811  fununfun  6573  dffv2  6966  fliftcnv  7299  riotaprop  7384  elovmpt3rab1  7660  3xpexg  7739  orduniorsuc  7814  unielxp  8012  dmtpos  8222  tpossym  8242  oesuclem  8498  ercnv  8704  cnvct  9019  sucxpdom  9209  enp1i  9227  pwfilem  9265  3xpfi  9268  rankr1id  9822  cardnn  9937  alephnbtwn2  10044  alephsucdom  10051  cdainflem  10159  isfin4p1  10287  axcclem  10429  dmct  10496  mptct  10510  infxpidm  10534  fpwwe2lem8  10611  gchpwdom  10643  elwina  10659  elina  10660  rankcf  10750  ltexprlem4  11012  lem1  12046  ltdivp1i  12129  nn0le2x  12546  rpnnen1lem5  12993  eluzfz1  13547  fzpred  13588  uznfz  13626  fz0fzdiffz0  13653  fzctr  13656  flid  13829  modid0  13918  2txmodxeq0  13955  faclbnd3  14316  faclbnd4lem4  14320  bcn1  14337  hashfac  14483  repswsymballbi  14805  wrdlen2i  14967  dfrtrclrec2  15083  rtrclreclem3  15085  rtrclreclem4  15086  relexpindlem  15088  sqrtsq  15308  absrdbnd  15381  sqreulem  15399  sqreu  15400  bpoly2  16099  bpoly3  16100  gcd0id  16565  lcmgcdlem  16652  lcmftp  16682  dvdsnprmd  16736  2mulprm  16739  pcprod  16943  fldivp1  16945  invsym2  17808  pleval2i  18378  smndlsmidm  19714  gsumle  20203  subrgsubm  20658  resrhm2b  20675  pzriprnglem11  21598  znchr  21669  psrbagfsupp  22026  mattposvs  22569  smadiadetglem2  22786  tg1  23078  cldval  23137  cldss  23143  cldopn  23145  1stcrestlem  23566  refbas  23624  refssex  23625  regr1  23864  kqreg  23865  kqnrm  23866  ufilen  24044  efmndtmd  24215  symgtgp  24220  psmetdmdm  24419  icoopnst  25055  cnheiborlem  25070  cfilfcls  25390  eflogeq  26721  logdivlt  26740  logdifbnd  27112  harmonicbnd4  27129  basellem5  27203  bposlem7  27408  zabsle1  27414  addsqn2reu  27559  chto1ub  27594  chpo1ub  27598  vmadivsum  27600  dchrmusum2  27612  dchrvmasum2if  27615  dchrvmasumlema  27618  dchrvmasumiflem2  27620  dchrisum0re  27631  dchrvmasumlem  27641  rplogsum  27645  mulogsumlem  27649  logdivsum  27651  selberg2lem  27668  pntrmax  27682  pntlem3  27727  pntleml  27729  pnt2  27731  noextendlt  27787  usgredg2vlem2  29481  vtxdgelxnn0  29727  wlkonprop  29911  wksonproplem  29957  wwlknbp  30096  wspthnp  30104  wlklnwwlkln1  30122  clwwlkf  30303  erclwwlknsym  30326  erclwwlkntr  30327  eupth0  30470  numclwwlk1lem2fo  30614  numclwlk2lem2f  30633  numclwwlk5lem  30643  hilablo  31417  hhssabloilem  31518  mayete3i  31985  homullid  32057  adjeu  32146  lnopeqi  32265  cnlnadjlem7  32330  adjbdlnb  32341  nmopcoadji  32358  bracnlnval  32371  mptctf  32969  xraddge02  33010  xrge0npcan  33248  gsumvsca1  33454  gsumvsca2  33455  baselsiga  34417  sigasspw  34418  ddeval1  34536  ddeval0  34537  braew  34544  derangen2  35532  subfaclim  35546  snmlff  35687  elfzm12  36033  fnetr  36719  wl-sbal1  38073  poimirlem13  38139  poimirlem14  38140  poimirlem31  38157  poimirlem32  38158  ismblfin  38167  itg2addnclem2  38178  areacirclem2  38215  areacirc  38219  ismgmOLD  38356  ismndo2  38380  rngomndo  38441  ecxrn2  38914  dmqseq  39230  prter3  39513  atbase  39920  llnbase  40140  lplnbase  40165  lvolbase  40209  lhpbase  40629  rernegcl  42987  renegadd  42988  reneg0addlid  42990  sn-0ne2  43022  3cubes  43278  mzpsubmpt  43331  mzpnegmpt  43332  eliunov2  44262  iunrelexp0  44285  enmappwid  44583  uunT1  45347  nnfoctb  45627  rn1st  45847  afveu  47746  afv2eu  47831  afv20fv0  47856  fzopredsuc  47917  fargshiftfva  48048  lindsrng01  49100  cic1st2nd  49677  cicpropdlem  49679  zeroo2  49864