Theorem impcom 410

Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypothesis

Ref	Expression
imp.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
impcom	⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Proof of Theorem impcom

Step	Hyp	Ref	Expression
1		imp.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 32	. 2 ⊢ (𝜓 → (𝜑 → 𝜒))
3	2	imp 409	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:  mpan9  509  bianir  1053  19.29r  1869  19.41v  1944  19.41  2230  nfsb4t  2533  nfsb4tALT  2598  mo4  2644  2euexv  2710  2euex  2720  gencl  3533  2gencl  3534  vtocl2ga  3573  vtocl4g  3577  rspccva  3620  2reurex  3748  2reu1  3879  rexdifi  4120  sseq0  4351  r19.2z  4438  falseral0  4457  elelpwi  4552  preqsnd  4781  prproe  4828  ssuni  4852  disji2  5039  invdisjrab  5043  disjiun  5044  disjxiun  5054  trintss  5180  ssexg  5218  reusv2lem3  5291  propeqop  5388  otiunsndisj  5401  rexopabb  5406  pofun  5484  solin  5491  2optocl  5639  3optocl  5640  ssrelrn  5756  elrnmpt1  5823  resieq  5857  reuop  6137  funimaexg  6433  fnun  6456  fss  6520  fun  6533  fvelimab  6730  fvmptss  6773  fvn0ssdmfun  6835  fvcofneq  6852  fmptco  6884  funsndifnop  6906  fnressn  6913  fressnfv  6915  fvn0fvelrn  6918  fmptsng  6923  fvtp2g  6954  fvtp3g  6955  tpres  6956  fnex  6972  funfvima3  6990  isores3  7080  dmfex  7633  opreuopreu  7726  releldmdifi  7736  funeldmdif  7739  el2mpocsbcl  7772  f1o2ndf1  7810  frxp  7812  fnse  7819  ressuppssdif  7843  funsssuppss  7848  suppss  7852  mpoxopxnop0  7873  reldmtpos  7892  wfrfun  7957  wfrlem12  7958  smores  7981  tfrlem7  8011  tz7.48-2  8070  tz7.49  8073  oacl  8152  omcl  8153  oecl  8154  oarec  8180  oewordri  8210  oeworde  8211  oelim2  8213  oeoa  8215  oeoelem  8216  oeoe  8217  nnacl  8229  nnmcl  8230  nnecl  8231  nnmsucr  8243  2ecoptocl  8380  undifixp  8490  ssct  8590  xpf1o  8671  limensuc  8686  ac6sfi  8754  frfi  8755  difinf  8780  f1dmvrnfibi  8800  f1vrnfibi  8801  suppeqfsuppbi  8839  elfiun  8886  dffi3  8887  infsupprpr  8960  xpwdomg  9041  infdiffi  9113  epfrs  9165  rankxpsuc  9303  updjud  9355  tskwe  9371  infxpenlem  9431  fseqenlem1  9442  kmlem2  9569  cff1  9672  cflim2  9677  sornom  9691  infpssrlem4  9720  fin23lem26  9739  fin23lem30  9756  fin23lem34  9760  isf32lem11  9777  fin67  9809  isfin7-2  9810  fin1a2lem10  9823  axcc2lem  9850  axdc2lem  9862  axdc3lem2  9865  axdc3lem4  9867  axdc4lem  9869  iunfo  9953  tsk0  10177  gruina  10232  grur1a  10233  mulcanenq  10374  reclem2pr  10462  supsrlem  10525  supsr  10526  ax1rid  10575  negf1o  11062  mulgt1  11491  fiminreOLD  11582  lbreu  11583  nnaddcl  11652  nnmulcl  11653  nn0n0n1ge2b  11955  nn0indd  12071  fzind  12072  fnn0ind  12073  uzaddcl  12296  uzinfi  12320  nn01to3  12333  elpq  12366  xmulasslem2  12667  supxrunb1  12704  supxrunb2  12705  infmremnf  12728  infmrp1  12729  uzsubsubfz  12921  elfz0ubfz0  13003  fz0fzdiffz0  13008  elfzmlbp  13010  fzofzim  13076  elfzom1elp1fzo  13096  ssfzo12bi  13124  fzonfzoufzol  13132  elfznelfzob  13135  injresinjlem  13149  injresinj  13150  modaddmodup  13294  modfzo0difsn  13303  modsumfzodifsn  13304  addmodlteq  13306  om2uzlti  13310  fsequb  13335  ssnn0fi  13345  ser1const  13418  expcllem  13432  expeq0  13451  expmordi  13523  expnngt1  13594  faclbnd  13642  hashf1rn  13705  hashgadd  13730  hashunx  13739  hashnn0n0nn  13744  hashgt0elex  13754  hashss  13762  hashfzp1  13784  hashxp  13787  hashmap  13788  hashimarni  13794  seqcoll  13814  hash2exprb  13821  hashge2el2difr  13831  elss2prb  13837  hashdifsnp1  13846  fi1uzind  13847  brfi1indALT  13850  lswlgt0cl  13913  swrdnd  14008  swrdnnn0nd  14010  swrdnd0  14011  swrd0  14012  swrdsbslen  14018  swrdspsleq  14019  pfxsuff1eqwrdeq  14053  swrdswrdlem  14058  swrdswrd  14059  wrd2ind  14077  pfxccatin12lem2a  14081  swrdccatin2  14083  pfxccatin12lem2  14085  pfxccatin12lem3  14086  pfxccatin12  14087  pfxccat3  14088  swrdccat  14089  pfxccat3a  14092  swrdccat3blem  14093  repswswrd  14138  repswrevw  14141  cshwmodn  14149  cshwsublen  14150  cshwidxmod  14157  cshwidxmodr  14158  cshf1  14164  2cshw  14167  cshweqrep  14175  cshw1  14176  2cshwcshw  14179  cshwcshid  14181  cshwcsh2id  14182  wrdlen2i  14296  2swrd2eqwrdeq  14307  wwlktovfo  14314  relexpsucnnl  14383  rtrclreclem3  14411  rtrclreclem4  14412  relexpindlem  14414  r19.29uz  14702  caubnd  14710  sqreu  14712  climshft  14925  climub  15010  climserle  15011  sumss  15073  sumss2  15075  modfsummods  15140  o1fsum  15160  binom  15177  climcndslem1  15196  climcndslem2  15197  pwm1geoserOLD  15217  cvgrat  15231  clim2prod  15236  prodfn0  15242  prodfrec  15243  ntrivcvgfvn0  15247  fprodn0  15325  fprodmodd  15343  fprodefsum  15440  demoivreALT  15546  ruclem8  15582  dvdsaddre2b  15649  dvdsdivcl  15658  dvdsfac  15668  oddnn02np1  15689  oddge22np1  15690  evennn02n  15691  evennn2n  15692  m1exp1  15719  nn0o  15726  pwp1fsum  15734  flodddiv4  15756  smu01lem  15826  dvdslegcd  15845  gcdneg  15862  dfgcd2  15886  gcdmultipleOLD  15892  seq1st  15907  alginv  15911  lcmf  15969  lcmftp  15972  lcmfunsnlem2lem2  15975  lcmfunsnlem  15977  lcmfun  15981  ncoprmgcdne1b  15986  coprmproddvdslem  15998  coprmproddvds  15999  cncongr1  16003  prmdvdsexp  16051  prmndvdsfaclt  16059  ncoprmlnprm  16060  fvprmselgcd1  16373  prmgaplem6  16384  prmgaplem7  16385  prmgaplem8  16386  cshwshashlem1  16421  setsstruct2  16513  setsstruct  16515  inveq  17036  catsubcat  17101  initoeu2lem0  17265  initoeu2lem1  17266  funcestrcsetclem8  17389  funcestrcsetclem9  17390  fthestrcsetc  17392  fullestrcsetc  17393  funcsetcestrclem9  17405  fthsetcestrc  17407  fullsetcestrc  17408  lubss  17723  lubel  17724  issstrmgm  17855  mgmb1mgm1  17857  sgrpidmnd  17908  frmdgsum  18019  smndex1mndlem  18066  mgm2nsgrplem3  18077  dfgrp2  18120  cyccom  18338  gaass  18419  gsumwrev  18486  symgextf1lem  18540  symgextf1  18541  fvcosymgeq  18549  gsmsymgreq  18552  symgfixelsi  18555  pmtrprfv3  18574  symggen  18590  pmtrprfval  18607  gsumzres  19021  gsumpr  19067  gsumzunsnd  19068  srgmulgass  19273  srgbinom  19287  lmodvsmmulgdi  19661  lmodfopnelem1  19662  rmodislmodlem  19693  0ringnnzr  20034  assamulgscm  20122  gsumply1subr  20394  gsummoncoe1  20464  pf1ind  20510  cnfldmulg  20569  cnfldexp  20570  psgndiflemB  20736  matmulcell  21046  mat1dimscm  21076  dmatmul  21098  dmatscmcl  21104  scmataddcl  21117  scmatsubcl  21118  scmatsgrp1  21123  mavmulsolcl  21152  ma1repveval  21172  1marepvmarrepid  21176  symgmatr01lem  21254  slesolvec  21280  cramerimplem2  21285  decpmatmullem  21371  pm2mpf1  21399  mp2pm2mplem4  21409  monmat2matmon  21424  chpscmat  21442  chpscmatgsumbin  21444  fvmptnn04ifb  21451  chfacfscmul0  21458  chfacfscmulgsum  21460  chfacfpmmul0  21462  chfacfpmmulgsum  21464  cpmadugsumlemF  21476  toprntopon  21525  clsss  21654  ntrss  21655  restntr  21782  cmpsublem  21999  cmpsub  22000  2ndcrest  22054  txindislem  22233  t0kq  22418  filufint  22520  fbflim2  22577  flftg  22596  alexsubALTlem4  22650  cnextfvval  22665  ustuqtop4  22845  xmettri2  22942  mettri  22954  metss  23110  tngngp3  23257  clmvscom  23686  lmmbr  23853  caublcls  23904  lmcau  23908  ovolunlem1a  24089  nulmbl2  24129  voliunlem1  24143  iunmbl  24146  volsup  24149  dvlip  24582  dvfsumle  24610  degltlem1  24658  ply1divex  24722  plyco  24823  dgrnznn  24829  dvnply2  24868  plydivex  24878  aannenlem2  24910  aaliou3lem2  24924  ulmcau  24975  zabsle1  25864  gausslemma2dlem1a  25933  gausslemma2dlem2  25935  gausslemma2dlem3  25936  gausslemma2dlem4  25937  2lgslem1a1  25957  2sqnn0  26006  2sqreulem1  26014  2sqreunnlem1  26017  dchrisumlem1  26057  dchrisumlem2  26058  dchrisumlem3  26059  qabvle  26193  ostthlem2  26196  ostth2lem2  26202  tgjustr  26252  axeuclidlem  26740  incistruhgr  26856  umgredgprv  26884  umgrpredgv  26917  usgredgprvALT  26969  uhgr2edg  26982  usgredg2vlem2  27000  lfuhgr1v0e  27028  subgrfun  27055  umgrres1lem  27084  upgrres1  27087  fusgrfis  27104  uhgrnbgr0nb  27128  nbgr1vtx  27132  nb3grprlem1  27154  uvtx01vtx  27171  fusgrn0degnn0  27273  vtxdginducedm1lem4  27316  finsumvtxdg2size  27324  wlkl1loop  27411  wlkres  27444  lfgrwlknloop  27463  pthdadjvtx  27503  upgr2pthnlp  27505  upgrwlkdvdelem  27509  upgrwlkdvde  27510  uhgrwkspthlem2  27527  usgr2trlspth  27534  usgr2pth  27537  pthdlem2lem  27540  lfgrn1cycl  27575  uspgrn2crct  27578  crctcshwlkn0lem3  27582  crctcshwlkn0lem4  27583  crctcshwlkn0lem5  27584  iswspthsnon  27626  wlkiswwlks1  27637  wlklnwwlkln1  27638  wlkiswwlks2  27645  wlkiswwlksupgr2  27647  wlklnwwlkln2lem  27652  wlknwwlksnbij  27658  wwlksnred  27662  wwlksnext  27663  wwlksnredwwlkn  27665  wwlksnredwwlkn0  27666  wwlksnextfun  27668  wwlksnextinj  27669  wwlksnextsurj  27670  wspthsnonn0vne  27688  wspn0  27695  wwlks2onv  27724  elwwlks2  27737  elwspths2spth  27738  rusgrnumwwlk  27746  clwwlkccatlem  27759  clwlkclwwlklem2a1  27762  clwlkclwwlklem2fv2  27766  clwlkclwwlklem2a4  27767  clwlkclwwlklem2a  27768  clwlkclwwlklem2  27770  clwlkclwwlkf1lem3  27776  clwwisshclwwslem  27784  clwwisshclwwsn  27786  erclwwlktr  27792  isclwwlknx  27806  clwwlkinwwlk  27810  clwwlkel  27817  clwwlkf  27818  clwwlkf1  27820  clwwlkfo  27821  clwwlkext2edg  27827  wwlksext2clwwlk  27828  wwlksubclwwlk  27829  clwwlknscsh  27833  erclwwlkntr  27842  eleclclwwlkn  27847  hashecclwwlkn1  27848  umgrhashecclwwlk  27849  clwwlknon0  27864  clwwlknonel  27866  clwwlknon1  27868  clwwlknonwwlknonb  27877  clwwlknonex2lem2  27879  clwwlknun  27883  clwwlkvbij  27884  upgr3v3e3cycl  27951  uhgr3cyclex  27953  upgr4cycl4dv4e  27956  eulerpath  28012  eucrctshift  28014  eucrct2eupth  28016  1to2vfriswmgr  28050  1to3vfriswmgr  28051  3cyclfrgrrn1  28056  4cycl2vnunb  28061  frgrwopreglem2  28084  frgrwopreglem3  28085  frgrwopreglem5ALT  28093  fusgr2wsp2nb  28105  2clwwlk2clwwlklem  28117  2clwwlk2clwwlk  28121  numclwwlk1lem2f1  28128  numclwwlk1lem2fo  28129  numclwwlk1  28132  clwwlknonclwlknonf1o  28133  dlwwlknondlwlknonf1o  28136  numclwlk1  28142  numclwlk2lem2f  28148  numclwlk2lem2f1o  28150  numclwwlk5  28159  frgrreg  28165  frgrregord013  28166  friendship  28170  nsnlplig  28250  nsnlpligALT  28251  isgrpo  28266  vcdi  28334  vcdir  28335  vcass  28336  nmosetre  28533  hlim2  28961  shscli  29086  chintcli  29100  dfch2  29176  spansncvi  29421  nmopsetretALT  29632  nmfnsetre  29646  lnopl  29683  lnfnl  29700  pjss2coi  29933  pjorthcoi  29938  pjscji  29939  pjssdif2i  29943  pjclem4a  29967  pj3lem1  29975  strlem5  30024  hstrlem5  30032  cvmdi  30093  mdslmd3i  30101  atcv1  30149  atcvat4i  30166  cdj3lem2a  30205  cdj3lem3a  30208  opreu2reuALT  30232  iuninc  30304  disji2f  30319  disjif2  30323  fmptcof2  30394  nnindd  30528  xrsmulgzz  30658  ofldchr  30880  esumfzf  31321  issgon  31375  voliune  31481  volfiniune  31482  rrvsum  31705  bnj228  31998  bnj1294  32082  bnj229  32149  bnj607  32181  bnj908  32196  bnj953  32204  bnj1118  32249  bnj1174  32268  bnj1388  32298  funen1cnv  32350  acycgrsubgr  32398  cvmliftlem15  32538  satfsschain  32604  satfdm  32609  satf0op  32617  fmla0xp  32623  gonarlem  32634  goalrlem  32636  satffunlem1lem1  32642  satffunlem2lem1  32644  dmopab3rexdif  32645  satefvfmla0  32658  prv1n  32671  iprodefisumlem  32965  faclimlem1  32968  dfon2lem6  33026  tfisg  33048  poseq  33088  frrlem8  33123  fpr2  33133  frr2  33138  noprefixmo  33195  nosupbnd1lem5  33205  nocvxminlem  33240  nocvxmin  33241  slerec  33270  idinside  33538  onsucconni  33778  axc11n11r  34010  bj-brrelex12ALT  34351  bj-snmoore  34397  bj-finsumval0  34559  exlimim  34615  exellim  34617  icoreclin  34630  difunieq  34647  fvineqsneq  34685  pibt2  34690  wl-spae  34753  wl-aleq  34767  fin2so  34871  matunitlindf  34882  poimirlem4  34888  poimirlem26  34910  itg2addnclem  34935  upixp  34996  welb  35003  sdclem2  35009  metf1o  35022  sstotbnd3  35046  isbndx  35052  ismtycnv  35072  heiborlem4  35084  bfplem1  35092  opidonOLD  35122  grpomndo  35145  ax12eq  36069  ax12el  36070  cvrat4  36571  mzpexpmpt  39332  diophren  39400  rmxypos  39534  jm2.17a  39547  jm2.17b  39548  rmygeid  39551  jm2.18  39575  jm2.25  39586  jm2.15nn0  39590  jm2.16nn0  39591  pwslnm  39684  isnumbasgrplem1  39691  dgraalem  39735  relexpiidm  40039  relexpmulnn  40044  relexpmulg  40045  relexp01min  40048  relexp0a  40051  relexpxpmin  40052  clsk1indlem3  40383  grucollcld  40586  dvgrat  40634  radcnvrat  40636  sspwimpcf  41244  sspwimpcfVD  41245  e2ebindALT  41253  eu2ndop1stv  43314  afvfv0bi  43341  afveu  43342  afvres  43361  aovmpt4g  43390  ndmaovass  43395  ndmaovdistr  43396  afv2orxorb  43417  afv2eu  43427  imarnf1pr  43471  nltle2tri  43503  fzopredsuc  43513  subsubelfzo0  43516  fzoopth  43517  2ffzoeq  43518  smonoord  43521  elsetpreimafvssdm  43536  iccpartres  43568  iccpartiltu  43572  iccpartigtl  43573  iccpartgt  43577  icceuelpartlem  43585  fargshiftf1  43591  ichnreuop  43624  ichreuopeq  43625  elsprel  43627  sprsymrelfo  43649  prproropf1olem4  43658  paireqne  43663  sbcpr  43673  reupr  43674  goldbachth  43699  fmtnoprmfac1  43717  fmtnoprmfac2  43719  prmdvdsfmtnof1lem2  43737  lighneallem2  43761  lighneallem4  43765  requad2  43778  even3prm2  43874  fpprwpprb  43895  gbegt5  43916  sbgoldbwt  43932  sbgoldbm  43939  nnsum3primesgbe  43947  wtgoldbnnsum4prm  43957  bgoldbnnsum3prm  43959  bgoldbtbndlem2  43961  bgoldbtbndlem3  43962  bgoldbtbndlem4  43963  bgoldbtbnd  43964  isomuspgrlem1  43982  isomuspgrlem2d  43986  upgrwlkupwlk  44005  uspgropssxp  44009  uspgrsprfo  44013  mgmpropd  44032  isassintop  44107  lidldomn1  44182  lidlmmgm  44186  2zlidl  44195  2zrngamgm  44200  2zrngmmgm  44207  rnghmsscmap  44235  rnghmsubcsetclem2  44237  rngcinv  44242  rngccatidALTV  44250  rngcinvALTV  44254  funcrngcsetc  44259  funcrngcsetcALT  44260  rhmsscmap  44281  rhmsubcsetclem2  44283  rhmsubcrngclem2  44289  ringcinv  44293  funcringcsetc  44296  funcringcsetcALTV2lem9  44305  ringccatidALTV  44313  ringcinvALTV  44317  srhmsubc  44337  rhmsubclem4  44350  srhmsubcALTV  44355  rhmsubcALTVlem4  44368  lmodvsmdi  44420  ply1mulgsumlem1  44430  ply1mulgsumlem2  44431  lincdifsn  44469  lincsumcl  44476  lincscmcl  44477  lincext3  44501  lindslinindsimp1  44502  lindslinindsimp2lem5  44507  snlindsntor  44516  lincresunit2  44523  lincresunit3lem2  44525  zgtp1leeq  44566  m1modmmod  44571  elbigo2  44602  fllog2  44618  digexp  44657  dig1  44658  nn0sumshdiglemA  44669  nn0sumshdiglemB  44670  rrxlinec  44713  eenglngeehlnm  44716  rrx2linest  44719  itsclc0yqsol  44741  itsclc0xyqsol  44745