Theorem mpancom 685

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 584	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 206  df-an 397

This theorem is referenced by:  mpan  687  spesbc  3816  csbie2df  4375  xpiindi  5747  fununfun  6489  dffv2  6872  elunirn2  7135  fliftcnv  7191  riotaprop  7269  elovmpt3rab1  7538  3xpexg  7611  orduniorsuc  7686  unielxp  7878  dmtpos  8063  tpossym  8083  wfrlem5OLD  8153  oesuclem  8364  ercnv  8528  cnvct  8833  undomOLD  8856  pwfilem  8969  sucxpdom  9041  3xpfi  9095  pwfilemOLD  9122  rankr1id  9629  cardnn  9730  alephnbtwn2  9837  alephsucdom  9844  cdainflem  9952  isfin4p1  10080  axcclem  10222  dmct  10289  mptct  10303  infxpidm  10327  fpwwe2lem8  10403  gchpwdom  10435  elwina  10451  elina  10452  rankcf  10542  ltexprlem4  10804  lem1  11827  ltdivp1i  11910  rpnnen1lem5  12730  eluzfz1  13272  fzpred  13313  uznfz  13348  fz0fzdiffz0  13374  fzctr  13377  flid  13537  modid0  13626  2txmodxeq0  13660  faclbnd3  14015  faclbnd4lem4  14019  bcn1  14036  hashfac  14181  repswsymballbi  14502  wrdlen2i  14664  dfrtrclrec2  14778  rtrclreclem3  14780  rtrclreclem4  14781  relexpindlem  14783  sqrtsq  14990  absrdbnd  15062  sqreulem  15080  sqreu  15081  bpoly2  15776  bpoly3  15777  gcd0id  16235  lcmgcdlem  16320  lcmftp  16350  dvdsnprmd  16404  2mulprm  16407  pcprod  16605  fldivp1  16607  invsym2  17484  pleval2i  18063  smndlsmidm  19270  subrgsubm  20046  cncrng  20628  znchr  20779  psrbagfsupp  21132  mattposvs  21613  smadiadetglem2  21830  tg1  22123  cldval  22183  cldss  22189  cldopn  22191  1stcrestlem  22612  refbas  22670  refssex  22671  regr1  22910  kqreg  22911  kqnrm  22912  ufilen  23090  efmndtmd  23261  symgtgp  23266  elrnust  23385  psmetdmdm  23467  metuval  23714  icoopnst  24111  cnheiborlem  24126  cfilfcls  24447  eflogeq  25766  logdivlt  25785  logdifbnd  26152  harmonicbnd4  26169  basellem5  26243  bposlem7  26447  zabsle1  26453  addsqn2reu  26598  chto1ub  26633  chpo1ub  26637  vmadivsum  26639  dchrmusum2  26651  dchrvmasum2if  26654  dchrvmasumlema  26657  dchrvmasumiflem2  26659  dchrisum0re  26670  dchrvmasumlem  26680  rplogsum  26684  mulogsumlem  26688  logdivsum  26690  selberg2lem  26707  pntrmax  26721  pntlem3  26766  pntleml  26768  pnt2  26770  usgredg2vlem2  27602  vtxdgelxnn0  27848  wlkonprop  28035  wksonproplem  28081  wksonproplemOLD  28082  wwlknbp  28216  wspthnp  28224  wlklnwwlkln1  28242  clwwlkf  28420  erclwwlknsym  28443  erclwwlkntr  28444  eupth0  28587  numclwwlk1lem2fo  28731  numclwlk2lem2f  28750  numclwwlk5lem  28760  hilablo  29531  hhssabloilem  29632  mayete3i  30099  homulid2  30171  adjeu  30260  lnopeqi  30379  cnlnadjlem7  30444  adjbdlnb  30455  nmopcoadji  30472  bracnlnval  30485  mptctf  31061  xraddge02  31088  xrge0npcan  31312  gsumle  31359  gsumvsca1  31488  gsumvsca2  31489  metidval  31849  pstmval  31854  baselsiga  32092  sigasspw  32093  ddeval1  32211  ddeval0  32212  braew  32219  derangen2  33145  subfaclim  33159  snmlff  33300  elfzm12  33642  noextendlt  33881  madebdaylemlrcut  34088  fnetr  34549  wl-sbal1  35727  poimirlem13  35799  poimirlem14  35800  poimirlem31  35817  poimirlem32  35818  ismblfin  35827  itg2addnclem2  35838  areacirclem2  35875  areacirc  35879  ismgmOLD  36017  ismndo2  36041  rngomndo  36102  cnvepimaex  36478  dmqseq  36760  prter3  36903  atbase  37310  llnbase  37530  lplnbase  37555  lvolbase  37599  lhpbase  38019  rernegcl  40361  renegadd  40362  reneg0addid2  40364  sn-0ne2  40396  3cubes  40519  mzpsubmpt  40572  mzpnegmpt  40573  eliunov2  41294  iunrelexp0  41317  enmappwid  41615  uunT1  42407  nnfoctb  42602  afveu  44656  afv2eu  44741  afv20fv0  44766  fzopredsuc  44826  fargshiftfva  44906  lindsrng01  45820