Theorem impcom 407

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 406	1 ⊢ ((𝜓 ∧ 𝜑) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 396

This theorem is referenced by:  mpan9  506  bianir  1055  19.29r  1878  19.41v  1954  19.41  2231  nfsb4t  2503  mo4  2566  2euexv  2633  2euex  2643  raleqbidvv  3329  gencl  3461  2gencl  3462  vtocl2ga  3504  vtocl4g  3509  rspccva  3551  2reurex  3690  2reu1  3826  rexdifi  4076  sseq0  4330  r19.2z  4422  ralf0  4441  falseral0  4447  elelpwi  4542  preqsnd  4786  prproe  4834  ssuni  4863  disji2  5052  invdisjrab  5056  disjiun  5057  disjxiun  5067  trintss  5204  ssexg  5242  reusv2lem3  5318  propeqop  5415  otiunsndisj  5428  rexopabb  5434  pofun  5512  solin  5519  2optocl  5672  3optocl  5673  ssrelrn  5792  elrnmpt1  5856  resieq  5891  reuop  6185  funimaexg  6504  fnun  6529  fss  6601  fun  6620  fvelimab  6823  fvmptss  6869  fvn0ssdmfun  6934  fvcofneq  6951  fmptco  6983  funsndifnop  7005  fnressn  7012  fressnfv  7014  fvn0fvelrn  7017  fmptsng  7022  fvtp2g  7056  fvtp3g  7057  tpres  7058  fnex  7075  funfvima3  7094  isores3  7186  dmfex  7728  opreuopreu  7849  releldmdifi  7859  funeldmdif  7862  el2mpocsbcl  7896  f1o2ndf1  7934  frxp  7938  fnse  7945  ressuppssdif  7972  funsssuppss  7977  suppssOLD  7982  mpoxopxnop0  8002  reldmtpos  8021  frrlem8  8080  fpr2a  8089  wfrfunOLD  8121  wfrlem12OLD  8122  smores  8154  tfrlem7  8185  tz7.48-2  8243  tz7.49  8246  oacl  8327  omcl  8328  oecl  8329  oarec  8355  oewordri  8385  oeworde  8386  oelim2  8388  oeoa  8390  oeoelem  8391  oeoe  8392  nnacl  8404  nnmcl  8405  nnecl  8406  nnmsucr  8418  2ecoptocl  8555  fsetprcnex  8608  undifixp  8680  ssct  8793  xpf1o  8875  limensuc  8890  unfi  8917  imafi  8920  ac6sfi  8988  frfi  8989  difinf  9014  f1dmvrnfibi  9033  f1vrnfibi  9034  suppeqfsuppbi  9072  elfiun  9119  dffi3  9120  infsupprpr  9193  xpwdomg  9274  infdiffi  9346  epfrs  9420  frr2  9449  rankxpsuc  9571  updjud  9623  tskwe  9639  infxpenlem  9700  fseqenlem1  9711  kmlem2  9838  nnadju  9884  cff1  9945  cflim2  9950  sornom  9964  infpssrlem4  9993  fin23lem26  10012  fin23lem30  10029  fin23lem34  10033  isf32lem11  10050  fin67  10082  isfin7-2  10083  fin1a2lem10  10096  axcc2lem  10123  axdc2lem  10135  axdc3lem2  10138  axdc3lem4  10140  axdc4lem  10142  iunfo  10226  tsk0  10450  gruina  10505  grur1a  10506  mulcanenq  10647  reclem2pr  10735  supsrlem  10798  supsr  10799  ax1rid  10848  negf1o  11335  mulgt1  11764  lbreu  11855  nnindd  11923  nnaddcl  11926  nnmulcl  11927  nn0n0n1ge2b  12231  nn0indd  12347  fzind  12348  fnn0ind  12349  uzaddcl  12573  uzinfi  12597  nn01to3  12610  elpq  12644  xmulasslem2  12945  supxrunb1  12982  supxrunb2  12983  infmremnf  13006  infmrp1  13007  uzsubsubfz  13207  elfz0ubfz0  13289  fz0fzdiffz0  13294  elfzmlbp  13296  fzofzim  13362  elfzom1elp1fzo  13382  ssfzo12bi  13410  fzonfzoufzol  13418  elfznelfzob  13421  injresinjlem  13435  injresinj  13436  modaddmodup  13582  modfzo0difsn  13591  modsumfzodifsn  13592  addmodlteq  13594  om2uzlti  13598  fsequb  13623  ssnn0fi  13633  ser1const  13707  expcllem  13721  expeq0  13741  expmordi  13813  expnngt1  13884  faclbnd  13932  hashf1rn  13995  hashgadd  14020  hashunx  14029  hashnn0n0nn  14034  hashgt0elex  14044  hashss  14052  hashfzp1  14074  hashxp  14077  hashmap  14078  hashimarni  14084  seqcoll  14106  hash2exprb  14113  hashge2el2difr  14123  elss2prb  14129  hashdifsnp1  14138  fi1uzind  14139  brfi1indALT  14142  lswlgt0cl  14200  swrdnd  14295  swrdnnn0nd  14297  swrdnd0  14298  swrd0  14299  swrdsbslen  14305  swrdspsleq  14306  pfxsuff1eqwrdeq  14340  swrdswrdlem  14345  swrdswrd  14346  wrd2ind  14364  pfxccatin12lem2a  14368  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12lem3  14373  pfxccatin12  14374  pfxccat3  14375  swrdccat  14376  pfxccat3a  14379  swrdccat3blem  14380  repswswrd  14425  repswrevw  14428  cshwmodn  14436  cshwsublen  14437  cshwidxmod  14444  cshwidxmodr  14445  cshf1  14451  2cshw  14454  cshweqrep  14462  cshw1  14463  2cshwcshw  14466  cshwcshid  14468  cshwcsh2id  14469  wrdlen2i  14583  2swrd2eqwrdeq  14594  wwlktovfo  14601  relexpsucnnl  14669  rtrclreclem3  14699  rtrclreclem4  14700  relexpindlem  14702  r19.29uz  14990  caubnd  14998  sqreu  15000  climshft  15213  climub  15301  climserle  15302  sumss  15364  sumss2  15366  modfsummods  15433  o1fsum  15453  binom  15470  climcndslem1  15489  climcndslem2  15490  cvgrat  15523  clim2prod  15528  prodfn0  15534  prodfrec  15535  ntrivcvgfvn0  15539  fprodn0  15617  fprodmodd  15635  fprodefsum  15732  demoivreALT  15838  ruclem8  15874  dvdsaddre2b  15944  dvdsdivcl  15953  dvdsfac  15963  oddnn02np1  15985  oddge22np1  15986  evennn02n  15987  evennn2n  15988  m1exp1  16013  nn0o  16020  pwp1fsum  16028  flodddiv4  16050  smu01lem  16120  dvdslegcd  16139  gcdneg  16157  dfgcd2  16182  gcdmultipleOLD  16188  seq1st  16204  alginv  16208  lcmf  16266  lcmftp  16269  lcmfunsnlem2lem2  16272  lcmfunsnlem  16274  lcmfun  16278  ncoprmgcdne1b  16283  coprmproddvdslem  16295  coprmproddvds  16296  cncongr1  16300  prmdvdsexp  16348  prmndvdsfaclt  16358  ncoprmlnprm  16360  fvprmselgcd1  16674  prmgaplem6  16685  prmgaplem7  16686  prmgaplem8  16687  cshwshashlem1  16725  setsstruct2  16803  setsstruct  16805  inveq  17403  catsubcat  17470  initoeu2lem0  17644  initoeu2lem1  17645  funcestrcsetclem8  17780  funcestrcsetclem9  17781  fthestrcsetc  17783  fullestrcsetc  17784  funcsetcestrclem9  17796  fthsetcestrc  17798  fullsetcestrc  17799  lubss  18146  lubel  18147  issstrmgm  18252  mgmb1mgm1  18254  sgrpidmnd  18305  frmdgsum  18416  smndex1mndlem  18463  mgm2nsgrplem3  18474  dfgrp2  18519  cyccom  18737  gaass  18818  gsumwrev  18888  symgextf1lem  18943  symgextf1  18944  fvcosymgeq  18952  gsmsymgreq  18955  symgfixelsi  18958  pmtrprfv3  18977  symggen  18993  pmtrprfval  19010  gsumzres  19425  gsumpr  19471  gsumzunsnd  19472  srgmulgass  19682  srgbinom  19696  lmodvsmmulgdi  20073  lmodfopnelem1  20074  rmodislmodlem  20105  0ringnnzr  20453  cnfldmulg  20542  cnfldexp  20543  psgndiflemB  20717  assamulgscm  21015  gsumply1subr  21315  gsummoncoe1  21385  pf1ind  21431  matmulcell  21502  mat1dimscm  21532  dmatmul  21554  dmatscmcl  21560  scmataddcl  21573  scmatsubcl  21574  scmatsgrp1  21579  mavmulsolcl  21608  ma1repveval  21628  1marepvmarrepid  21632  symgmatr01lem  21710  slesolvec  21736  cramerimplem2  21741  decpmatmullem  21828  pm2mpf1  21856  mp2pm2mplem4  21866  monmat2matmon  21881  chpscmat  21899  chpscmatgsumbin  21901  fvmptnn04ifb  21908  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulgsum  21921  cpmadugsumlemF  21933  toprntopon  21982  clsss  22113  ntrss  22114  restntr  22241  cmpsublem  22458  cmpsub  22459  2ndcrest  22513  txindislem  22692  t0kq  22877  filufint  22979  fbflim2  23036  flftg  23055  alexsubALTlem4  23109  cnextfvval  23124  ustuqtop4  23304  xmettri2  23401  mettri  23413  metss  23570  tngngp3  23726  clmvscom  24159  lmmbr  24327  caublcls  24378  lmcau  24382  ovolunlem1a  24565  nulmbl2  24605  voliunlem1  24619  iunmbl  24622  volsup  24625  dvlip  25062  dvfsumle  25090  degltlem1  25142  ply1divex  25206  plyco  25307  dgrnznn  25313  dvnply2  25352  plydivex  25362  aannenlem2  25394  aaliou3lem2  25408  ulmcau  25459  zabsle1  26349  gausslemma2dlem1a  26418  gausslemma2dlem2  26420  gausslemma2dlem3  26421  gausslemma2dlem4  26422  2lgslem1a1  26442  2sqnn0  26491  2sqreulem1  26499  2sqreunnlem1  26502  dchrisumlem1  26542  dchrisumlem2  26543  dchrisumlem3  26544  qabvle  26678  ostthlem2  26681  ostth2lem2  26687  tgjustr  26739  axeuclidlem  27233  incistruhgr  27352  umgredgprv  27380  umgrpredgv  27413  usgredgprvALT  27465  uhgr2edg  27478  usgredg2vlem2  27496  lfuhgr1v0e  27524  subgrfun  27551  umgrres1lem  27580  upgrres1  27583  fusgrfis  27600  uhgrnbgr0nb  27624  nbgr1vtx  27628  nb3grprlem1  27650  uvtx01vtx  27667  fusgrn0degnn0  27769  vtxdginducedm1lem4  27812  finsumvtxdg2size  27820  wlkl1loop  27907  wlkres  27940  lfgrwlknloop  27959  pthdadjvtx  27999  upgr2pthnlp  28001  upgrwlkdvdelem  28005  upgrwlkdvde  28006  uhgrwkspthlem2  28023  usgr2trlspth  28030  usgr2pth  28033  pthdlem2lem  28036  lfgrn1cycl  28071  uspgrn2crct  28074  crctcshwlkn0lem3  28078  crctcshwlkn0lem4  28079  crctcshwlkn0lem5  28080  iswspthsnon  28122  wlkiswwlks1  28133  wlklnwwlkln1  28134  wlkiswwlks2  28141  wlkiswwlksupgr2  28143  wlklnwwlkln2lem  28148  wlknwwlksnbij  28154  wwlksnred  28158  wwlksnext  28159  wwlksnredwwlkn  28161  wwlksnredwwlkn0  28162  wwlksnextfun  28164  wwlksnextinj  28165  wwlksnextsurj  28166  wspthsnonn0vne  28183  wspn0  28190  wwlks2onv  28219  elwwlks2  28232  elwspths2spth  28233  rusgrnumwwlk  28241  clwwlkccatlem  28254  clwlkclwwlklem2a1  28257  clwlkclwwlklem2fv2  28261  clwlkclwwlklem2a4  28262  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwlkclwwlkf1lem3  28271  clwwisshclwwslem  28279  clwwisshclwwsn  28281  erclwwlktr  28287  isclwwlknx  28301  clwwlkinwwlk  28305  clwwlkel  28311  clwwlkf  28312  clwwlkf1  28314  clwwlkfo  28315  clwwlkext2edg  28321  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  clwwlknscsh  28327  erclwwlkntr  28336  eleclclwwlkn  28341  hashecclwwlkn1  28342  umgrhashecclwwlk  28343  clwwlknon0  28358  clwwlknonel  28360  clwwlknon1  28362  clwwlknonwwlknonb  28371  clwwlknonex2lem2  28373  clwwlknun  28377  clwwlkvbij  28378  upgr3v3e3cycl  28445  uhgr3cyclex  28447  upgr4cycl4dv4e  28450  eulerpath  28506  eucrctshift  28508  eucrct2eupth  28510  1to2vfriswmgr  28544  1to3vfriswmgr  28545  3cyclfrgrrn1  28550  4cycl2vnunb  28555  frgrwopreglem2  28578  frgrwopreglem3  28579  frgrwopreglem5ALT  28587  fusgr2wsp2nb  28599  2clwwlk2clwwlklem  28611  2clwwlk2clwwlk  28615  numclwwlk1lem2f1  28622  numclwwlk1lem2fo  28623  numclwwlk1  28626  clwwlknonclwlknonf1o  28627  dlwwlknondlwlknonf1o  28630  numclwlk1  28636  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  numclwwlk5  28653  frgrreg  28659  frgrregord013  28660  friendship  28664  nsnlplig  28744  nsnlpligALT  28745  isgrpo  28760  vcdi  28828  vcdir  28829  vcass  28830  nmosetre  29027  hlim2  29455  shscli  29580  chintcli  29594  dfch2  29670  spansncvi  29915  nmopsetretALT  30126  nmfnsetre  30140  lnopl  30177  lnfnl  30194  pjss2coi  30427  pjorthcoi  30432  pjscji  30433  pjssdif2i  30437  pjclem4a  30461  pj3lem1  30469  strlem5  30518  hstrlem5  30526  cvmdi  30587  mdslmd3i  30595  atcv1  30643  atcvat4i  30660  cdj3lem2a  30699  cdj3lem3a  30702  opreu2reuALT  30726  iuninc  30801  disji2f  30817  disjif2  30821  fmptcof2  30896  xrsmulgzz  31189  ofldchr  31415  esumfzf  31937  issgon  31991  voliune  32097  volfiniune  32098  rrvsum  32321  bnj228  32614  bnj1294  32697  bnj229  32764  bnj607  32796  bnj908  32811  bnj953  32819  bnj1118  32864  bnj1174  32883  bnj1388  32913  funen1cnv  32960  acycgrsubgr  33020  cvmliftlem15  33160  satfsschain  33226  satfdm  33231  satf0op  33239  fmla0xp  33245  gonarlem  33256  goalrlem  33258  satffunlem1lem1  33264  satffunlem2lem1  33266  dmopab3rexdif  33267  satefvfmla0  33280  prv1n  33293  iprodefisumlem  33612  faclimlem1  33615  dfon2lem6  33670  tfisg  33692  ttrclselem2  33712  frxp2  33718  frxp3  33724  poseq  33729  nosupbnd1lem5  33842  noinfbnd1lem5  33857  nocvxminlem  33899  nocvxmin  33900  slerec  33940  madebdaylemold  34005  idinside  34313  onsucconni  34553  axc11n11r  34792  bj-brrelex12ALT  35165  bj-snmoore  35211  bj-finsumval0  35383  exlimim  35440  exellim  35442  icoreclin  35455  difunieq  35472  fvineqsneq  35510  pibt2  35515  wl-spae  35607  wl-aleq  35621  fin2so  35691  matunitlindf  35702  poimirlem4  35708  poimirlem26  35730  itg2addnclem  35755  upixp  35814  welb  35821  sdclem2  35827  metf1o  35840  sstotbnd3  35861  isbndx  35867  ismtycnv  35887  heiborlem4  35899  bfplem1  35907  opidonOLD  35937  grpomndo  35960  ax12eq  36882  ax12el  36883  cvrat4  37384  mzpexpmpt  40483  diophren  40551  rmxypos  40685  jm2.17a  40698  jm2.17b  40699  rmygeid  40702  jm2.18  40726  jm2.25  40737  jm2.15nn0  40741  jm2.16nn0  40742  pwslnm  40835  isnumbasgrplem1  40842  dgraalem  40886  relexpiidm  41201  relexpmulnn  41206  relexpmulg  41207  relexp01min  41210  relexp0a  41213  relexpxpmin  41214  clsk1indlem3  41542  grucollcld  41767  dvgrat  41819  radcnvrat  41821  sspwimpcf  42429  sspwimpcfVD  42430  e2ebindALT  42438  fsetprcnexALT  44443  eu2ndop1stv  44504  afvfv0bi  44531  afveu  44532  afvres  44551  aovmpt4g  44580  ndmaovass  44585  ndmaovdistr  44586  afv2orxorb  44607  afv2eu  44617  imarnf1pr  44661  nltle2tri  44693  fzopredsuc  44703  subsubelfzo0  44706  fzoopth  44707  2ffzoeq  44708  smonoord  44711  elsetpreimafvssdm  44726  iccpartres  44758  iccpartiltu  44762  iccpartigtl  44763  iccpartgt  44767  icceuelpartlem  44775  fargshiftf1  44781  ichnreuop  44812  ichreuopeq  44813  elsprel  44815  sprsymrelfo  44837  prproropf1olem4  44846  paireqne  44851  sbcpr  44861  reupr  44862  goldbachth  44887  fmtnoprmfac1  44905  fmtnoprmfac2  44907  prmdvdsfmtnof1lem2  44925  lighneallem2  44946  lighneallem4  44950  requad2  44963  even3prm2  45059  fpprwpprb  45080  gbegt5  45101  sbgoldbwt  45117  sbgoldbm  45124  nnsum3primesgbe  45132  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  bgoldbtbnd  45149  isomuspgrlem1  45167  isomuspgrlem2d  45171  upgrwlkupwlk  45190  uspgropssxp  45194  uspgrsprfo  45198  mgmpropd  45217  isassintop  45292  lidldomn1  45367  lidlmmgm  45371  2zlidl  45380  2zrngamgm  45385  2zrngmmgm  45392  rnghmsscmap  45420  rnghmsubcsetclem2  45422  rngcinv  45427  rngccatidALTV  45435  rngcinvALTV  45439  funcrngcsetc  45444  funcrngcsetcALT  45445  rhmsscmap  45466  rhmsubcsetclem2  45468  rhmsubcrngclem2  45474  ringcinv  45478  funcringcsetc  45481  funcringcsetcALTV2lem9  45490  ringccatidALTV  45498  ringcinvALTV  45502  srhmsubc  45522  rhmsubclem4  45535  srhmsubcALTV  45540  rhmsubcALTVlem4  45553  lmodvsmdi  45606  ply1mulgsumlem1  45615  ply1mulgsumlem2  45616  lincdifsn  45653  lincsumcl  45660  lincscmcl  45661  lincext3  45685  lindslinindsimp1  45686  lindslinindsimp2lem5  45691  snlindsntor  45700  lincresunit2  45707  lincresunit3lem2  45709  zgtp1leeq  45750  m1modmmod  45755  elbigo2  45786  fllog2  45802  digexp  45841  dig1  45842  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854  1arymaptf1  45876  2arymaptf1  45887  rrxlinec  45970  eenglngeehlnm  45973  rrx2linest  45976  itsclc0yqsol  45998  itsclc0xyqsol  46002