Theorem impcom 409

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  mpan9  508  bianir  1057  19.29r  1877  19.41v  1953  19.41  2228  nfsb4t  2502  mo4  2565  2euexv  2632  2euex  2642  raleqbidvv  3302  gencl  3481  2gencl  3482  vtocl2ga  3526  vtocl4g  3531  rspccva  3572  2reurex  3709  2reu1  3844  rexdifi  4096  sseq0  4350  r19.2z  4443  ralf0  4462  falseral0  4468  elelpwi  4561  preqsnd  4807  prproe  4854  ssuni  4884  disji2  5078  invdisjrab  5082  disjiun  5083  disjxiun  5093  trintss  5232  ssexg  5271  reusv2lem3  5347  propeqop  5455  otiunsndisj  5468  rexopabb  5476  pofun  5554  solin  5561  2optocl  5717  3optocl  5718  ssrelrn  5840  elrnmpt1  5903  resieq  5938  reuop  6235  funimaexgOLD  6575  fnun  6601  fss  6672  fun  6691  fvelimab  6901  fvmptss  6947  fvn0ssdmfun  7012  fvcofneq  7029  fmptco  7061  funsndifnop  7083  fnressn  7090  fressnfv  7092  fvn0fvelrnOLD  7095  fmptsng  7100  fvtp2g  7134  fvtp3g  7135  tpres  7136  fnex  7153  funfvima3  7172  isores3  7266  tfisg  7772  dmfex  7826  opreuopreu  7948  releldmdifi  7958  funeldmdif  7961  el2mpocsbcl  7997  f1o2ndf1  8034  frxp  8038  fnse  8045  poseq  8049  ressuppssdif  8075  funsssuppss  8080  suppssOLD  8085  mpoxopxnop0  8105  reldmtpos  8124  frrlem8  8183  fpr2a  8192  wfrfunOLD  8224  wfrlem12OLD  8225  smores  8257  tfrlem7  8288  tz7.48-2  8347  tz7.49  8350  oacl  8440  omcl  8441  oecl  8442  oarec  8468  oewordri  8498  oeworde  8499  oelim2  8501  oeoa  8503  oeoelem  8504  oeoe  8505  nnacl  8517  nnmcl  8518  nnecl  8519  nnmsucr  8531  2ecoptocl  8672  fsetprcnex  8725  undifixp  8797  ssctOLD  8921  xpf1o  9008  limensuc  9023  unfi  9041  imafi  9044  en1eqsn  9143  ac6sfi  9156  frfi  9157  difinf  9185  f1dmvrnfibi  9205  f1vrnfibi  9206  suppeqfsuppbi  9244  elfiun  9291  dffi3  9292  infsupprpr  9365  xpwdomg  9446  infdiffi  9519  ttrclselem2  9587  epfrs  9592  frmin  9610  frr2  9621  rankxpsuc  9743  updjud  9795  tskwe  9811  infxpenlem  9874  fseqenlem1  9885  kmlem2  10012  nnadju  10058  cff1  10119  cflim2  10124  sornom  10138  infpssrlem4  10167  fin23lem26  10186  fin23lem30  10203  fin23lem34  10207  isf32lem11  10224  fin67  10256  isfin7-2  10257  fin1a2lem10  10270  axcc2lem  10297  axdc2lem  10309  axdc3lem2  10312  axdc3lem4  10314  axdc4lem  10316  iunfo  10400  tsk0  10624  gruina  10679  grur1a  10680  mulcanenq  10821  reclem2pr  10909  supsrlem  10972  supsr  10973  ax1rid  11022  negf1o  11510  mulgt1  11939  lbreu  12030  nnindd  12098  nnaddcl  12101  nnmulcl  12102  nn0n0n1ge2b  12406  nn0indd  12522  fzind  12523  fnn0ind  12524  uzaddcl  12749  uzinfi  12773  nn01to3  12786  elpq  12820  xmulasslem2  13121  supxrunb1  13158  supxrunb2  13159  infmremnf  13182  infmrp1  13183  uzsubsubfz  13383  elfz0ubfz0  13465  fz0fzdiffz0  13470  elfzmlbp  13472  fzofzim  13539  elfzom1elp1fzo  13559  ssfzo12bi  13587  fzonfzoufzol  13595  elfznelfzob  13598  injresinjlem  13612  injresinj  13613  modaddmodup  13759  modfzo0difsn  13768  modsumfzodifsn  13769  addmodlteq  13771  om2uzlti  13775  fsequb  13800  ssnn0fi  13810  ser1const  13884  expcllem  13898  expeq0  13918  expmordi  13990  expnngt1  14061  faclbnd  14109  hashf1rn  14171  hashgadd  14196  hashunx  14205  hashnn0n0nn  14210  hashgt0elex  14220  hashss  14228  hashfzp1  14250  hashxp  14253  hashmap  14254  hashimarni  14260  seqcoll  14282  hash2exprb  14289  hashge2el2difr  14299  elss2prb  14305  hashdifsnp1  14314  fi1uzind  14315  brfi1indALT  14318  lswlgt0cl  14376  swrdnd  14465  swrdnnn0nd  14467  swrdnd0  14468  swrd0  14469  swrdsbslen  14475  swrdspsleq  14476  pfxsuff1eqwrdeq  14510  swrdswrdlem  14515  swrdswrd  14516  wrd2ind  14534  pfxccatin12lem2a  14538  swrdccatin2  14540  pfxccatin12lem2  14542  pfxccatin12lem3  14543  pfxccatin12  14544  pfxccat3  14545  swrdccat  14546  pfxccat3a  14549  swrdccat3blem  14550  repswswrd  14595  repswrevw  14598  cshwmodn  14606  cshwsublen  14607  cshwidxmod  14614  cshwidxmodr  14615  cshf1  14621  2cshw  14624  cshweqrep  14632  cshw1  14633  2cshwcshw  14637  cshwcshid  14639  cshwcsh2id  14640  wrdlen2i  14754  2swrd2eqwrdeq  14765  wwlktovfo  14772  relexpsucnnl  14840  rtrclreclem3  14870  rtrclreclem4  14871  relexpindlem  14873  r19.29uz  15161  caubnd  15169  sqreu  15171  climshft  15384  climub  15472  climserle  15473  sumss  15535  sumss2  15537  modfsummods  15604  o1fsum  15624  binom  15641  climcndslem1  15660  climcndslem2  15661  cvgrat  15694  clim2prod  15699  prodfn0  15705  prodfrec  15706  ntrivcvgfvn0  15710  fprodn0  15788  fprodmodd  15806  fprodefsum  15903  demoivreALT  16009  ruclem8  16045  dvdsaddre2b  16115  dvdsdivcl  16124  dvdsfac  16134  oddnn02np1  16156  oddge22np1  16157  evennn02n  16158  evennn2n  16159  m1exp1  16184  nn0o  16191  pwp1fsum  16199  flodddiv4  16221  smu01lem  16291  dvdslegcd  16310  gcdneg  16328  dfgcd2  16353  seq1st  16373  alginv  16377  lcmf  16435  lcmftp  16438  lcmfunsnlem2lem2  16441  lcmfunsnlem  16443  lcmfun  16447  ncoprmgcdne1b  16452  coprmproddvdslem  16464  coprmproddvds  16465  cncongr1  16469  prmdvdsexp  16517  prmndvdsfaclt  16527  ncoprmlnprm  16529  fvprmselgcd1  16843  prmgaplem6  16854  prmgaplem7  16855  prmgaplem8  16856  cshwshashlem1  16894  setsstruct2  16972  setsstruct  16974  inveq  17583  catsubcat  17651  initoeu2lem0  17825  initoeu2lem1  17826  funcestrcsetclem8  17961  funcestrcsetclem9  17962  fthestrcsetc  17964  fullestrcsetc  17965  funcsetcestrclem9  17977  fthsetcestrc  17979  fullsetcestrc  17980  lubss  18328  lubel  18329  issstrmgm  18434  mgmb1mgm1  18436  sgrpidmnd  18487  frmdgsum  18597  smndex1mndlem  18644  mgm2nsgrplem3  18655  dfgrp2  18700  cyccom  18918  gaass  18999  gsumwrev  19069  symgextf1lem  19124  symgextf1  19125  fvcosymgeq  19133  gsmsymgreq  19136  symgfixelsi  19139  pmtrprfv3  19158  symggen  19174  pmtrprfval  19191  gsumzres  19604  gsumpr  19650  gsumzunsnd  19651  srgmulgass  19861  srgbinom  19875  lmodvsmmulgdi  20263  lmodfopnelem1  20264  rmodislmodlem  20295  0ringnnzr  20645  cnfldmulg  20735  cnfldexp  20736  psgndiflemB  20910  assamulgscm  21210  gsumply1subr  21510  gsummoncoe1  21580  pf1ind  21626  matmulcell  21699  mat1dimscm  21729  dmatmul  21751  dmatscmcl  21757  scmataddcl  21770  scmatsubcl  21771  scmatsgrp1  21776  mavmulsolcl  21805  ma1repveval  21825  1marepvmarrepid  21829  symgmatr01lem  21907  slesolvec  21933  cramerimplem2  21938  decpmatmullem  22025  pm2mpf1  22053  mp2pm2mplem4  22063  monmat2matmon  22078  chpscmat  22096  chpscmatgsumbin  22098  fvmptnn04ifb  22105  chfacfscmul0  22112  chfacfscmulgsum  22114  chfacfpmmul0  22116  chfacfpmmulgsum  22118  cpmadugsumlemF  22130  toprntopon  22179  clsss  22310  ntrss  22311  restntr  22438  cmpsublem  22655  cmpsub  22656  2ndcrest  22710  txindislem  22889  t0kq  23074  filufint  23176  fbflim2  23233  flftg  23252  alexsubALTlem4  23306  cnextfvval  23321  ustuqtop4  23501  xmettri2  23598  mettri  23610  metss  23769  tngngp3  23925  clmvscom  24358  lmmbr  24527  caublcls  24578  lmcau  24582  ovolunlem1a  24765  nulmbl2  24805  voliunlem1  24819  iunmbl  24822  volsup  24825  dvlip  25262  dvfsumle  25290  degltlem1  25342  ply1divex  25406  plyco  25507  dgrnznn  25513  dvnply2  25552  plydivex  25562  aannenlem2  25594  aaliou3lem2  25608  ulmcau  25659  zabsle1  26549  gausslemma2dlem1a  26618  gausslemma2dlem2  26620  gausslemma2dlem3  26621  gausslemma2dlem4  26622  2lgslem1a1  26642  2sqnn0  26691  2sqreulem1  26699  2sqreunnlem1  26702  dchrisumlem1  26742  dchrisumlem2  26743  dchrisumlem3  26744  qabvle  26878  ostthlem2  26881  ostth2lem2  26887  nosupbnd1lem5  26965  noinfbnd1lem5  26980  nocvxminlem  27022  nocvxmin  27023  slerec  27063  tgjustr  27123  axeuclidlem  27618  incistruhgr  27737  umgredgprv  27765  umgrpredgv  27798  usgredgprvALT  27850  uhgr2edg  27863  usgredg2vlem2  27881  lfuhgr1v0e  27909  subgrfun  27936  umgrres1lem  27965  upgrres1  27968  fusgrfis  27985  uhgrnbgr0nb  28009  nbgr1vtx  28013  nb3grprlem1  28035  uvtx01vtx  28052  fusgrn0degnn0  28154  vtxdginducedm1lem4  28197  finsumvtxdg2size  28205  wlkl1loop  28293  wlkres  28325  lfgrwlknloop  28344  pthdadjvtx  28385  upgr2pthnlp  28387  upgrwlkdvdelem  28391  upgrwlkdvde  28392  uhgrwkspthlem2  28409  usgr2trlspth  28416  usgr2pth  28419  pthdlem2lem  28422  lfgrn1cycl  28457  uspgrn2crct  28460  crctcshwlkn0lem3  28464  crctcshwlkn0lem4  28465  crctcshwlkn0lem5  28466  iswspthsnon  28508  wlkiswwlks1  28519  wlklnwwlkln1  28520  wlkiswwlks2  28527  wlkiswwlksupgr2  28529  wlklnwwlkln2lem  28534  wlknwwlksnbij  28540  wwlksnred  28544  wwlksnext  28545  wwlksnredwwlkn  28547  wwlksnredwwlkn0  28548  wwlksnextfun  28550  wwlksnextinj  28551  wwlksnextsurj  28552  wspthsnonn0vne  28569  wspn0  28576  wwlks2onv  28605  elwwlks2  28618  elwspths2spth  28619  rusgrnumwwlk  28627  clwwlkccatlem  28640  clwlkclwwlklem2a1  28643  clwlkclwwlklem2fv2  28647  clwlkclwwlklem2a4  28648  clwlkclwwlklem2a  28649  clwlkclwwlklem2  28651  clwlkclwwlkf1lem3  28657  clwwisshclwwslem  28665  clwwisshclwwsn  28667  erclwwlktr  28673  isclwwlknx  28687  clwwlkinwwlk  28691  clwwlkel  28697  clwwlkf  28698  clwwlkf1  28700  clwwlkfo  28701  clwwlkext2edg  28707  wwlksext2clwwlk  28708  wwlksubclwwlk  28709  clwwlknscsh  28713  erclwwlkntr  28722  eleclclwwlkn  28727  hashecclwwlkn1  28728  umgrhashecclwwlk  28729  clwwlknon0  28744  clwwlknonel  28746  clwwlknon1  28748  clwwlknonwwlknonb  28757  clwwlknonex2lem2  28759  clwwlknun  28763  clwwlkvbij  28764  upgr3v3e3cycl  28831  uhgr3cyclex  28833  upgr4cycl4dv4e  28836  eulerpath  28892  eucrctshift  28894  eucrct2eupth  28896  1to2vfriswmgr  28930  1to3vfriswmgr  28931  3cyclfrgrrn1  28936  4cycl2vnunb  28941  frgrwopreglem2  28964  frgrwopreglem3  28965  frgrwopreglem5ALT  28973  fusgr2wsp2nb  28985  2clwwlk2clwwlklem  28997  2clwwlk2clwwlk  29001  numclwwlk1lem2f1  29008  numclwwlk1lem2fo  29009  numclwwlk1  29012  clwwlknonclwlknonf1o  29013  dlwwlknondlwlknonf1o  29016  numclwlk1  29022  numclwlk2lem2f  29028  numclwlk2lem2f1o  29030  numclwwlk5  29039  frgrreg  29045  frgrregord013  29046  friendship  29050  nsnlplig  29130  nsnlpligALT  29131  isgrpo  29146  vcdi  29214  vcdir  29215  vcass  29216  nmosetre  29413  hlim2  29841  shscli  29966  chintcli  29980  dfch2  30056  spansncvi  30301  nmopsetretALT  30512  nmfnsetre  30526  lnopl  30563  lnfnl  30580  pjss2coi  30813  pjorthcoi  30818  pjscji  30819  pjssdif2i  30823  pjclem4a  30847  pj3lem1  30855  strlem5  30904  hstrlem5  30912  cvmdi  30973  mdslmd3i  30981  atcv1  31029  atcvat4i  31046  cdj3lem2a  31085  cdj3lem3a  31088  opreu2reuALT  31112  iuninc  31185  disji2f  31201  disjif2  31205  fmptcof2  31279  xrsmulgzz  31572  ofldchr  31811  esumfzf  32333  issgon  32387  voliune  32493  volfiniune  32494  rrvsum  32719  bnj228  33012  bnj1294  33094  bnj229  33161  bnj607  33193  bnj908  33208  bnj953  33216  bnj1118  33261  bnj1174  33280  bnj1388  33310  funen1cnv  33357  acycgrsubgr  33417  cvmliftlem15  33557  satfsschain  33623  satfdm  33628  satf0op  33636  fmla0xp  33642  gonarlem  33653  goalrlem  33655  satffunlem1lem1  33661  satffunlem2lem1  33663  dmopab3rexdif  33664  satefvfmla0  33677  prv1n  33690  iprodefisumlem  33996  faclimlem1  33999  dfon2lem6  34047  frxp2  34073  frxp3  34079  madebdaylemold  34186  idinside  34523  onsucconni  34763  axc11n11r  35002  bj-brrelex12ALT  35392  bj-snmoore  35438  bj-finsumval0  35610  exlimim  35667  exellim  35669  icoreclin  35682  difunieq  35699  fvineqsneq  35737  pibt2  35742  wl-spae  35834  wl-aleq  35848  fin2so  35920  matunitlindf  35931  poimirlem4  35937  poimirlem26  35959  itg2addnclem  35984  upixp  36043  welb  36050  sdclem2  36056  metf1o  36069  sstotbnd3  36090  isbndx  36096  ismtycnv  36116  heiborlem4  36128  bfplem1  36136  opidonOLD  36166  grpomndo  36189  ax12eq  37259  ax12el  37260  cvrat4  37762  mzpexpmpt  40880  diophren  40948  rmxypos  41083  jm2.17a  41096  jm2.17b  41097  rmygeid  41100  jm2.18  41124  jm2.25  41135  jm2.15nn0  41139  jm2.16nn0  41140  pwslnm  41233  isnumbasgrplem1  41240  dgraalem  41284  relexpiidm  41685  relexpmulnn  41690  relexpmulg  41691  relexp01min  41694  relexp0a  41697  relexpxpmin  41698  clsk1indlem3  42026  grucollcld  42251  dvgrat  42303  radcnvrat  42305  sspwimpcf  42913  sspwimpcfVD  42914  e2ebindALT  42922  et-sqrtnegnre  44792  fsetprcnexALT  44974  eu2ndop1stv  45035  afvfv0bi  45062  afveu  45063  afvres  45082  aovmpt4g  45111  ndmaovass  45116  ndmaovdistr  45117  afv2orxorb  45138  afv2eu  45148  imarnf1pr  45192  nltle2tri  45223  fzopredsuc  45233  subsubelfzo0  45236  fzoopth  45237  2ffzoeq  45238  smonoord  45241  elsetpreimafvssdm  45256  iccpartres  45288  iccpartiltu  45292  iccpartigtl  45293  iccpartgt  45297  icceuelpartlem  45305  fargshiftf1  45311  ichnreuop  45342  ichreuopeq  45343  elsprel  45345  sprsymrelfo  45367  prproropf1olem4  45376  paireqne  45381  sbcpr  45391  reupr  45392  goldbachth  45417  fmtnoprmfac1  45435  fmtnoprmfac2  45437  prmdvdsfmtnof1lem2  45455  lighneallem2  45476  lighneallem4  45480  requad2  45493  even3prm2  45589  fpprwpprb  45610  gbegt5  45631  sbgoldbwt  45647  sbgoldbm  45654  nnsum3primesgbe  45662  wtgoldbnnsum4prm  45672  bgoldbnnsum3prm  45674  bgoldbtbndlem2  45676  bgoldbtbndlem3  45677  bgoldbtbndlem4  45678  bgoldbtbnd  45679  isomuspgrlem1  45697  isomuspgrlem2d  45701  upgrwlkupwlk  45720  uspgropssxp  45724  uspgrsprfo  45728  mgmpropd  45747  isassintop  45822  lidldomn1  45897  lidlmmgm  45901  2zlidl  45910  2zrngamgm  45915  2zrngmmgm  45922  rnghmsscmap  45950  rnghmsubcsetclem2  45952  rngcinv  45957  rngccatidALTV  45965  rngcinvALTV  45969  funcrngcsetc  45974  funcrngcsetcALT  45975  rhmsscmap  45996  rhmsubcsetclem2  45998  rhmsubcrngclem2  46004  funcringcsetc  46011  funcringcsetcALTV2lem9  46020  ringccatidALTV  46028  srhmsubc  46052  rhmsubclem4  46065  srhmsubcALTV  46070  rhmsubcALTVlem4  46083  lmodvsmdi  46136  ply1mulgsumlem1  46145  ply1mulgsumlem2  46146  lincdifsn  46183  lincsumcl  46190  lincscmcl  46191  lincext3  46215  lindslinindsimp1  46216  lindslinindsimp2lem5  46221  snlindsntor  46230  lincresunit2  46237  lincresunit3lem2  46239  zgtp1leeq  46280  m1modmmod  46285  elbigo2  46316  fllog2  46332  digexp  46371  dig1  46372  nn0sumshdiglemA  46383  nn0sumshdiglemB  46384  1arymaptf1  46406  2arymaptf1  46417  rrxlinec  46500  eenglngeehlnm  46503  rrx2linest  46506  itsclc0yqsol  46528  itsclc0xyqsol  46532