Theorem impcom 408

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 407	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:  mpan9  507  bianir  1056  19.29r  1878  19.41v  1954  19.41  2229  nfsb4t  2504  mo4  2567  2euexv  2634  2euex  2644  raleqbidvv  3339  gencl  3472  2gencl  3473  vtocl2ga  3515  vtocl4g  3520  rspccva  3561  2reurex  3696  2reu1  3831  rexdifi  4081  sseq0  4334  r19.2z  4426  ralf0  4445  falseral0  4451  elelpwi  4546  preqsnd  4790  prproe  4838  ssuni  4867  disji2  5057  invdisjrab  5061  disjiun  5062  disjxiun  5072  trintss  5209  ssexg  5248  reusv2lem3  5324  propeqop  5422  otiunsndisj  5435  rexopabb  5442  pofun  5522  solin  5529  2optocl  5683  3optocl  5684  ssrelrn  5806  elrnmpt1  5870  resieq  5905  reuop  6200  funimaexgOLD  6528  fnun  6554  fss  6626  fun  6645  fvelimab  6850  fvmptss  6896  fvn0ssdmfun  6961  fvcofneq  6978  fmptco  7010  funsndifnop  7032  fnressn  7039  fressnfv  7041  fvn0fvelrn  7044  fmptsng  7049  fvtp2g  7083  fvtp3g  7084  tpres  7085  fnex  7102  funfvima3  7121  isores3  7215  dmfex  7763  opreuopreu  7885  releldmdifi  7895  funeldmdif  7898  el2mpocsbcl  7934  f1o2ndf1  7972  frxp  7976  fnse  7983  ressuppssdif  8010  funsssuppss  8015  suppssOLD  8020  mpoxopxnop0  8040  reldmtpos  8059  frrlem8  8118  fpr2a  8127  wfrfunOLD  8159  wfrlem12OLD  8160  smores  8192  tfrlem7  8223  tz7.48-2  8282  tz7.49  8285  oacl  8374  omcl  8375  oecl  8376  oarec  8402  oewordri  8432  oeworde  8433  oelim2  8435  oeoa  8437  oeoelem  8438  oeoe  8439  nnacl  8451  nnmcl  8452  nnecl  8453  nnmsucr  8465  2ecoptocl  8606  fsetprcnex  8659  undifixp  8731  ssct  8848  xpf1o  8935  limensuc  8950  unfi  8964  imafi  8967  ac6sfi  9067  frfi  9068  difinf  9093  f1dmvrnfibi  9112  f1vrnfibi  9113  suppeqfsuppbi  9151  elfiun  9198  dffi3  9199  infsupprpr  9272  xpwdomg  9353  infdiffi  9425  ttrclselem2  9493  epfrs  9498  frmin  9516  frr2  9527  rankxpsuc  9649  updjud  9701  tskwe  9717  infxpenlem  9778  fseqenlem1  9789  kmlem2  9916  nnadju  9962  cff1  10023  cflim2  10028  sornom  10042  infpssrlem4  10071  fin23lem26  10090  fin23lem30  10107  fin23lem34  10111  isf32lem11  10128  fin67  10160  isfin7-2  10161  fin1a2lem10  10174  axcc2lem  10201  axdc2lem  10213  axdc3lem2  10216  axdc3lem4  10218  axdc4lem  10220  iunfo  10304  tsk0  10528  gruina  10583  grur1a  10584  mulcanenq  10725  reclem2pr  10813  supsrlem  10876  supsr  10877  ax1rid  10926  negf1o  11414  mulgt1  11843  lbreu  11934  nnindd  12002  nnaddcl  12005  nnmulcl  12006  nn0n0n1ge2b  12310  nn0indd  12426  fzind  12427  fnn0ind  12428  uzaddcl  12653  uzinfi  12677  nn01to3  12690  elpq  12724  xmulasslem2  13025  supxrunb1  13062  supxrunb2  13063  infmremnf  13086  infmrp1  13087  uzsubsubfz  13287  elfz0ubfz0  13369  fz0fzdiffz0  13374  elfzmlbp  13376  fzofzim  13443  elfzom1elp1fzo  13463  ssfzo12bi  13491  fzonfzoufzol  13499  elfznelfzob  13502  injresinjlem  13516  injresinj  13517  modaddmodup  13663  modfzo0difsn  13672  modsumfzodifsn  13673  addmodlteq  13675  om2uzlti  13679  fsequb  13704  ssnn0fi  13714  ser1const  13788  expcllem  13802  expeq0  13822  expmordi  13894  expnngt1  13965  faclbnd  14013  hashf1rn  14076  hashgadd  14101  hashunx  14110  hashnn0n0nn  14115  hashgt0elex  14125  hashss  14133  hashfzp1  14155  hashxp  14158  hashmap  14159  hashimarni  14165  seqcoll  14187  hash2exprb  14194  hashge2el2difr  14204  elss2prb  14210  hashdifsnp1  14219  fi1uzind  14220  brfi1indALT  14223  lswlgt0cl  14281  swrdnd  14376  swrdnnn0nd  14378  swrdnd0  14379  swrd0  14380  swrdsbslen  14386  swrdspsleq  14387  pfxsuff1eqwrdeq  14421  swrdswrdlem  14426  swrdswrd  14427  wrd2ind  14445  pfxccatin12lem2a  14449  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12lem3  14454  pfxccatin12  14455  pfxccat3  14456  swrdccat  14457  pfxccat3a  14460  swrdccat3blem  14461  repswswrd  14506  repswrevw  14509  cshwmodn  14517  cshwsublen  14518  cshwidxmod  14525  cshwidxmodr  14526  cshf1  14532  2cshw  14535  cshweqrep  14543  cshw1  14544  2cshwcshw  14547  cshwcshid  14549  cshwcsh2id  14550  wrdlen2i  14664  2swrd2eqwrdeq  14675  wwlktovfo  14682  relexpsucnnl  14750  rtrclreclem3  14780  rtrclreclem4  14781  relexpindlem  14783  r19.29uz  15071  caubnd  15079  sqreu  15081  climshft  15294  climub  15382  climserle  15383  sumss  15445  sumss2  15447  modfsummods  15514  o1fsum  15534  binom  15551  climcndslem1  15570  climcndslem2  15571  cvgrat  15604  clim2prod  15609  prodfn0  15615  prodfrec  15616  ntrivcvgfvn0  15620  fprodn0  15698  fprodmodd  15716  fprodefsum  15813  demoivreALT  15919  ruclem8  15955  dvdsaddre2b  16025  dvdsdivcl  16034  dvdsfac  16044  oddnn02np1  16066  oddge22np1  16067  evennn02n  16068  evennn2n  16069  m1exp1  16094  nn0o  16101  pwp1fsum  16109  flodddiv4  16131  smu01lem  16201  dvdslegcd  16220  gcdneg  16238  dfgcd2  16263  gcdmultipleOLD  16269  seq1st  16285  alginv  16289  lcmf  16347  lcmftp  16350  lcmfunsnlem2lem2  16353  lcmfunsnlem  16355  lcmfun  16359  ncoprmgcdne1b  16364  coprmproddvdslem  16376  coprmproddvds  16377  cncongr1  16381  prmdvdsexp  16429  prmndvdsfaclt  16439  ncoprmlnprm  16441  fvprmselgcd1  16755  prmgaplem6  16766  prmgaplem7  16767  prmgaplem8  16768  cshwshashlem1  16806  setsstruct2  16884  setsstruct  16886  inveq  17495  catsubcat  17563  initoeu2lem0  17737  initoeu2lem1  17738  funcestrcsetclem8  17873  funcestrcsetclem9  17874  fthestrcsetc  17876  fullestrcsetc  17877  funcsetcestrclem9  17889  fthsetcestrc  17891  fullsetcestrc  17892  lubss  18240  lubel  18241  issstrmgm  18346  mgmb1mgm1  18348  sgrpidmnd  18399  frmdgsum  18510  smndex1mndlem  18557  mgm2nsgrplem3  18568  dfgrp2  18613  cyccom  18831  gaass  18912  gsumwrev  18982  symgextf1lem  19037  symgextf1  19038  fvcosymgeq  19046  gsmsymgreq  19049  symgfixelsi  19052  pmtrprfv3  19071  symggen  19087  pmtrprfval  19104  gsumzres  19519  gsumpr  19565  gsumzunsnd  19566  srgmulgass  19776  srgbinom  19790  lmodvsmmulgdi  20167  lmodfopnelem1  20168  rmodislmodlem  20199  0ringnnzr  20549  cnfldmulg  20639  cnfldexp  20640  psgndiflemB  20814  assamulgscm  21114  gsumply1subr  21414  gsummoncoe1  21484  pf1ind  21530  matmulcell  21603  mat1dimscm  21633  dmatmul  21655  dmatscmcl  21661  scmataddcl  21674  scmatsubcl  21675  scmatsgrp1  21680  mavmulsolcl  21709  ma1repveval  21729  1marepvmarrepid  21733  symgmatr01lem  21811  slesolvec  21837  cramerimplem2  21842  decpmatmullem  21929  pm2mpf1  21957  mp2pm2mplem4  21967  monmat2matmon  21982  chpscmat  22000  chpscmatgsumbin  22002  fvmptnn04ifb  22009  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulgsum  22022  cpmadugsumlemF  22034  toprntopon  22083  clsss  22214  ntrss  22215  restntr  22342  cmpsublem  22559  cmpsub  22560  2ndcrest  22614  txindislem  22793  t0kq  22978  filufint  23080  fbflim2  23137  flftg  23156  alexsubALTlem4  23210  cnextfvval  23225  ustuqtop4  23405  xmettri2  23502  mettri  23514  metss  23673  tngngp3  23829  clmvscom  24262  lmmbr  24431  caublcls  24482  lmcau  24486  ovolunlem1a  24669  nulmbl2  24709  voliunlem1  24723  iunmbl  24726  volsup  24729  dvlip  25166  dvfsumle  25194  degltlem1  25246  ply1divex  25310  plyco  25411  dgrnznn  25417  dvnply2  25456  plydivex  25466  aannenlem2  25498  aaliou3lem2  25512  ulmcau  25563  zabsle1  26453  gausslemma2dlem1a  26522  gausslemma2dlem2  26524  gausslemma2dlem3  26525  gausslemma2dlem4  26526  2lgslem1a1  26546  2sqnn0  26595  2sqreulem1  26603  2sqreunnlem1  26606  dchrisumlem1  26646  dchrisumlem2  26647  dchrisumlem3  26648  qabvle  26782  ostthlem2  26785  ostth2lem2  26791  tgjustr  26844  axeuclidlem  27339  incistruhgr  27458  umgredgprv  27486  umgrpredgv  27519  usgredgprvALT  27571  uhgr2edg  27584  usgredg2vlem2  27602  lfuhgr1v0e  27630  subgrfun  27657  umgrres1lem  27686  upgrres1  27689  fusgrfis  27706  uhgrnbgr0nb  27730  nbgr1vtx  27734  nb3grprlem1  27756  uvtx01vtx  27773  fusgrn0degnn0  27875  vtxdginducedm1lem4  27918  finsumvtxdg2size  27926  wlkl1loop  28014  wlkres  28047  lfgrwlknloop  28066  pthdadjvtx  28107  upgr2pthnlp  28109  upgrwlkdvdelem  28113  upgrwlkdvde  28114  uhgrwkspthlem2  28131  usgr2trlspth  28138  usgr2pth  28141  pthdlem2lem  28144  lfgrn1cycl  28179  uspgrn2crct  28182  crctcshwlkn0lem3  28186  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  iswspthsnon  28230  wlkiswwlks1  28241  wlklnwwlkln1  28242  wlkiswwlks2  28249  wlkiswwlksupgr2  28251  wlklnwwlkln2lem  28256  wlknwwlksnbij  28262  wwlksnred  28266  wwlksnext  28267  wwlksnredwwlkn  28269  wwlksnredwwlkn0  28270  wwlksnextfun  28272  wwlksnextinj  28273  wwlksnextsurj  28274  wspthsnonn0vne  28291  wspn0  28298  wwlks2onv  28327  elwwlks2  28340  elwspths2spth  28341  rusgrnumwwlk  28349  clwwlkccatlem  28362  clwlkclwwlklem2a1  28365  clwlkclwwlklem2fv2  28369  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  clwlkclwwlkf1lem3  28379  clwwisshclwwslem  28387  clwwisshclwwsn  28389  erclwwlktr  28395  isclwwlknx  28409  clwwlkinwwlk  28413  clwwlkel  28419  clwwlkf  28420  clwwlkf1  28422  clwwlkfo  28423  clwwlkext2edg  28429  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  clwwlknscsh  28435  erclwwlkntr  28444  eleclclwwlkn  28449  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknon0  28466  clwwlknonel  28468  clwwlknon1  28470  clwwlknonwwlknonb  28479  clwwlknonex2lem2  28481  clwwlknun  28485  clwwlkvbij  28486  upgr3v3e3cycl  28553  uhgr3cyclex  28555  upgr4cycl4dv4e  28558  eulerpath  28614  eucrctshift  28616  eucrct2eupth  28618  1to2vfriswmgr  28652  1to3vfriswmgr  28653  3cyclfrgrrn1  28658  4cycl2vnunb  28663  frgrwopreglem2  28686  frgrwopreglem3  28687  frgrwopreglem5ALT  28695  fusgr2wsp2nb  28707  2clwwlk2clwwlklem  28719  2clwwlk2clwwlk  28723  numclwwlk1lem2f1  28730  numclwwlk1lem2fo  28731  numclwwlk1  28734  clwwlknonclwlknonf1o  28735  dlwwlknondlwlknonf1o  28738  numclwlk1  28744  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  numclwwlk5  28761  frgrreg  28767  frgrregord013  28768  friendship  28772  nsnlplig  28852  nsnlpligALT  28853  isgrpo  28868  vcdi  28936  vcdir  28937  vcass  28938  nmosetre  29135  hlim2  29563  shscli  29688  chintcli  29702  dfch2  29778  spansncvi  30023  nmopsetretALT  30234  nmfnsetre  30248  lnopl  30285  lnfnl  30302  pjss2coi  30535  pjorthcoi  30540  pjscji  30541  pjssdif2i  30545  pjclem4a  30569  pj3lem1  30577  strlem5  30626  hstrlem5  30634  cvmdi  30695  mdslmd3i  30703  atcv1  30751  atcvat4i  30768  cdj3lem2a  30807  cdj3lem3a  30810  opreu2reuALT  30834  iuninc  30909  disji2f  30925  disjif2  30929  fmptcof2  31003  xrsmulgzz  31296  ofldchr  31522  esumfzf  32046  issgon  32100  voliune  32206  volfiniune  32207  rrvsum  32430  bnj228  32723  bnj1294  32806  bnj229  32873  bnj607  32905  bnj908  32920  bnj953  32928  bnj1118  32973  bnj1174  32992  bnj1388  33022  funen1cnv  33069  acycgrsubgr  33129  cvmliftlem15  33269  satfsschain  33335  satfdm  33340  satf0op  33348  fmla0xp  33354  gonarlem  33365  goalrlem  33367  satffunlem1lem1  33373  satffunlem2lem1  33375  dmopab3rexdif  33376  satefvfmla0  33389  prv1n  33402  iprodefisumlem  33715  faclimlem1  33718  dfon2lem6  33773  tfisg  33795  frxp2  33800  frxp3  33806  poseq  33811  nosupbnd1lem5  33924  noinfbnd1lem5  33939  nocvxminlem  33981  nocvxmin  33982  slerec  34022  madebdaylemold  34087  idinside  34395  onsucconni  34635  axc11n11r  34874  bj-brrelex12ALT  35247  bj-snmoore  35293  bj-finsumval0  35465  exlimim  35522  exellim  35524  icoreclin  35537  difunieq  35554  fvineqsneq  35592  pibt2  35597  wl-spae  35689  wl-aleq  35703  fin2so  35773  matunitlindf  35784  poimirlem4  35790  poimirlem26  35812  itg2addnclem  35837  upixp  35896  welb  35903  sdclem2  35909  metf1o  35922  sstotbnd3  35943  isbndx  35949  ismtycnv  35969  heiborlem4  35981  bfplem1  35989  opidonOLD  36019  grpomndo  36042  ax12eq  36962  ax12el  36963  cvrat4  37464  mzpexpmpt  40574  diophren  40642  rmxypos  40776  jm2.17a  40789  jm2.17b  40790  rmygeid  40793  jm2.18  40817  jm2.25  40828  jm2.15nn0  40832  jm2.16nn0  40833  pwslnm  40926  isnumbasgrplem1  40933  dgraalem  40977  relexpiidm  41319  relexpmulnn  41324  relexpmulg  41325  relexp01min  41328  relexp0a  41331  relexpxpmin  41332  clsk1indlem3  41660  grucollcld  41885  dvgrat  41937  radcnvrat  41939  sspwimpcf  42547  sspwimpcfVD  42548  e2ebindALT  42556  fsetprcnexALT  44567  eu2ndop1stv  44628  afvfv0bi  44655  afveu  44656  afvres  44675  aovmpt4g  44704  ndmaovass  44709  ndmaovdistr  44710  afv2orxorb  44731  afv2eu  44741  imarnf1pr  44785  nltle2tri  44816  fzopredsuc  44826  subsubelfzo0  44829  fzoopth  44830  2ffzoeq  44831  smonoord  44834  elsetpreimafvssdm  44849  iccpartres  44881  iccpartiltu  44885  iccpartigtl  44886  iccpartgt  44890  icceuelpartlem  44898  fargshiftf1  44904  ichnreuop  44935  ichreuopeq  44936  elsprel  44938  sprsymrelfo  44960  prproropf1olem4  44969  paireqne  44974  sbcpr  44984  reupr  44985  goldbachth  45010  fmtnoprmfac1  45028  fmtnoprmfac2  45030  prmdvdsfmtnof1lem2  45048  lighneallem2  45069  lighneallem4  45073  requad2  45086  even3prm2  45182  fpprwpprb  45203  gbegt5  45224  sbgoldbwt  45240  sbgoldbm  45247  nnsum3primesgbe  45255  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbndlem4  45271  bgoldbtbnd  45272  isomuspgrlem1  45290  isomuspgrlem2d  45294  upgrwlkupwlk  45313  uspgropssxp  45317  uspgrsprfo  45321  mgmpropd  45340  isassintop  45415  lidldomn1  45490  lidlmmgm  45494  2zlidl  45503  2zrngamgm  45508  2zrngmmgm  45515  rnghmsscmap  45543  rnghmsubcsetclem2  45545  rngcinv  45550  rngccatidALTV  45558  rngcinvALTV  45562  funcrngcsetc  45567  funcrngcsetcALT  45568  rhmsscmap  45589  rhmsubcsetclem2  45591  rhmsubcrngclem2  45597  ringcinv  45601  funcringcsetc  45604  funcringcsetcALTV2lem9  45613  ringccatidALTV  45621  ringcinvALTV  45625  srhmsubc  45645  rhmsubclem4  45658  srhmsubcALTV  45663  rhmsubcALTVlem4  45676  lmodvsmdi  45729  ply1mulgsumlem1  45738  ply1mulgsumlem2  45739  lincdifsn  45776  lincsumcl  45783  lincscmcl  45784  lincext3  45808  lindslinindsimp1  45809  lindslinindsimp2lem5  45814  snlindsntor  45823  lincresunit2  45830  lincresunit3lem2  45832  zgtp1leeq  45873  m1modmmod  45878  elbigo2  45909  fllog2  45925  digexp  45964  dig1  45965  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977  1arymaptf1  45999  2arymaptf1  46010  rrxlinec  46093  eenglngeehlnm  46096  rrx2linest  46099  itsclc0yqsol  46121  itsclc0xyqsol  46125