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 207  df-an 396

This theorem is referenced by:  mpan9  506  bianir  1058  19.29r  1874  19.41v  1949  19.41  2236  nfsb4t  2497  mo4  2559  2euexv  2624  2euex  2634  raleqbidvvOLD  3308  gencl  3489  2gencl  3490  vtocl2ga  3544  vtocl2gaf  3545  vtocl3gaf  3547  vtocl3ga  3549  vtocl4g  3551  vtocl4ga  3552  rspccva  3587  2reurex  3731  2reu1  3860  rexdifi  4113  sseq0  4366  r19.2z  4458  ralf0  4477  falseral0  4479  elelpwi  4573  preqsnd  4823  prproe  4869  ssuni  4896  disji2  5091  disjiun  5095  disjxiun  5104  trintss  5233  ssexg  5278  reusv2lem3  5355  propeqop  5467  otiunsndisj  5480  rexopabb  5488  pofun  5564  solin  5573  2optocl  5734  3optocl  5735  ssrelrn  5858  elrnmpt1  5924  resieq  5961  imadifssran  6124  reuop  6266  funimaexgOLD  6604  fnun  6632  fss  6704  fun  6722  fvelimab  6933  fvmptss  6980  fvn0ssdmfun  7046  fvcofneq  7065  fmptco  7101  funsndifnop  7123  fnressn  7130  fressnfv  7132  fvn0fvelrnOLD  7135  fmptsng  7142  fvtp2g  7173  fvtp3g  7174  tpres  7175  fnex  7191  funfvima3  7210  fvf1pr  7282  isores3  7310  tfisg  7830  dmfex  7881  opreuopreu  8013  releldmdifi  8024  funeldmdif  8027  el2mpocsbcl  8064  f1o2ndf1  8101  frxp  8105  fnse  8112  frxp2  8123  frxp3  8130  poseq  8137  ressuppssdif  8164  funsssuppss  8169  mpoxopxnop0  8194  reldmtpos  8213  frrlem8  8272  fpr2a  8281  smores  8321  tfrlem7  8351  tz7.48-2  8410  tz7.49  8413  oacl  8499  omcl  8500  oecl  8501  oarec  8526  oewordri  8556  oeworde  8557  oelim2  8559  oeoa  8561  oeoelem  8562  oeoe  8563  nnacl  8575  nnmcl  8576  nnecl  8577  nnmsucr  8589  naddoa  8666  brinxper  8700  2ecoptocl  8781  fsetprcnex  8835  undifixp  8907  xpf1o  9103  limensuc  9118  unfi  9135  en1eqsn  9219  ac6sfi  9231  frfi  9232  difinf  9260  imafiOLD  9265  f1dmvrnfibi  9292  f1vrnfibi  9293  suppeqfsuppbi  9330  elfiun  9381  dffi3  9382  infsupprpr  9457  xpwdomg  9538  infdiffi  9611  ttrclselem2  9679  epfrs  9684  frmin  9702  frr2  9713  rankxpsuc  9835  updjud  9887  tskwe  9903  infxpenlem  9966  fseqenlem1  9977  kmlem2  10105  nnadju  10151  cff1  10211  cflim2  10216  sornom  10230  infpssrlem4  10259  fin23lem26  10278  fin23lem30  10295  fin23lem34  10299  isf32lem11  10316  fin67  10348  isfin7-2  10349  fin1a2lem10  10362  axcc2lem  10389  axdc2lem  10401  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  iunfo  10492  tsk0  10716  gruina  10771  grur1a  10772  mulcanenq  10913  reclem2pr  11001  supsrlem  11064  supsr  11065  ax1rid  11114  negf1o  11608  mulgt1OLD  12041  lbreu  12133  nnindd  12206  nnaddcl  12209  nnmulcl  12210  nn0n0n1ge2b  12511  nn0indd  12631  fzind  12632  fnn0ind  12633  uzaddcl  12863  uzinfi  12887  nn01to3  12900  elpq  12934  xmulasslem2  13242  supxrunb1  13279  supxrunb2  13280  infmremnf  13304  infmrp1  13305  uzsubsubfz  13507  fzdif1  13566  elfz0ubfz0  13593  fz0fzdiffz0  13598  elfzmlbp  13600  fzofzim  13670  elfzom1elp1fzo  13693  ssfzo12bi  13722  fzoopth  13723  fzonfzoufzol  13731  elfznelfzob  13734  injresinjlem  13748  injresinj  13749  modaddmodup  13899  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  om2uzlti  13915  fsequb  13940  ssnn0fi  13950  ser1const  14023  expcllem  14037  expeq0  14057  expmordi  14132  expnngt1  14206  faclbnd  14255  hashf1rn  14317  hashgadd  14342  hashunx  14351  hashnn0n0nn  14356  hashgt0elex  14366  hashss  14374  hashfzp1  14396  hashxp  14399  hashmap  14400  hashimarni  14406  seqcoll  14429  hash2exprb  14436  hashge2el2difr  14446  elss2prb  14453  hashdifsnp1  14471  fi1uzind  14472  brfi1indALT  14475  lswlgt0cl  14534  swrdnd  14619  swrdnnn0nd  14621  swrdnd0  14622  swrd0  14623  swrdsbslen  14629  swrdspsleq  14630  pfxsuff1eqwrdeq  14664  swrdswrdlem  14669  swrdswrd  14670  wrd2ind  14688  pfxccatin12lem2a  14692  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12lem3  14697  pfxccatin12  14698  pfxccat3  14699  swrdccat  14700  pfxccat3a  14703  swrdccat3blem  14704  repswswrd  14749  repswrevw  14752  cshwmodn  14760  cshwsublen  14761  cshwidxmod  14768  cshwidxmodr  14769  cshf1  14775  2cshw  14778  cshweqrep  14786  cshw1  14787  2cshwcshw  14791  cshwcshid  14793  cshwcsh2id  14794  wrdlen2i  14908  2swrd2eqwrdeq  14919  wwlktovfo  14924  relexpsucnnl  14996  rtrclreclem3  15026  rtrclreclem4  15027  relexpindlem  15029  r19.29uz  15317  caubnd  15325  sqreu  15327  climshft  15542  climub  15628  climserle  15629  sumss  15690  sumss2  15692  modfsummods  15759  o1fsum  15779  binom  15796  climcndslem1  15815  climcndslem2  15816  cvgrat  15849  clim2prod  15854  prodfn0  15860  prodfrec  15861  ntrivcvgfvn0  15865  fprodn0  15945  fprodmodd  15963  fprodefsum  16061  demoivreALT  16169  ruclem8  16205  dvdsaddre2b  16277  dvdsdivcl  16286  dvdsfac  16296  oddnn02np1  16318  oddge22np1  16319  evennn02n  16320  evennn2n  16321  m1exp1  16346  nn0o  16353  pwp1fsum  16361  flodddiv4  16385  smu01lem  16455  dvdslegcd  16474  gcdneg  16492  dfgcd2  16516  seq1st  16541  alginv  16545  lcmf  16603  lcmftp  16606  lcmfunsnlem2lem2  16609  lcmfunsnlem  16611  lcmfun  16615  ncoprmgcdne1b  16620  coprmproddvdslem  16632  coprmproddvds  16633  cncongr1  16637  prmdvdsexp  16685  prmndvdsfaclt  16695  ncoprmlnprm  16698  fvprmselgcd1  17016  prmgaplem6  17027  prmgaplem7  17028  prmgaplem8  17029  cshwshashlem1  17066  setsstruct2  17144  setsstruct  17146  inveq  17736  catsubcat  17801  initoeu2lem0  17975  initoeu2lem1  17976  funcestrcsetclem8  18108  funcestrcsetclem9  18109  fthestrcsetc  18111  fullestrcsetc  18112  funcsetcestrclem9  18124  fthsetcestrc  18126  fullsetcestrc  18127  lubss  18472  lubel  18473  mgmpropd  18578  issstrmgm  18580  mgmb1mgm1  18582  sgrpidmnd  18666  frmdgsum  18789  smndex1mndlem  18836  mgm2nsgrplem3  18847  dfgrp2  18894  cyccom  19135  gaass  19229  gsumwrev  19298  symgextf1lem  19350  symgextf1  19351  fvcosymgeq  19359  gsmsymgreq  19362  symgfixelsi  19365  pmtrprfv3  19384  symggen  19400  pmtrprfval  19417  gsumzres  19839  gsumpr  19885  gsumzunsnd  19886  srgmulgass  20126  srgbinom  20140  0ringnnzr  20434  rnghmsscmap  20539  rnghmsubcsetclem2  20541  rngcinv  20546  funcrngcsetc  20549  funcrngcsetcALT  20550  rhmsscmap  20568  rhmsubcsetclem2  20570  rhmsubcrngclem2  20576  funcringcsetc  20583  srhmsubc  20589  rhmsubclem4  20597  lmodvsmmulgdi  20803  lmodfopnelem1  20804  rmodislmodlem  20835  rngqiprngimfo  21211  cnfldmulg  21315  cnfldexp  21316  psgndiflemB  21509  assamulgscm  21810  gsumply1subr  22118  gsummoncoe1  22195  pf1ind  22242  matmulcell  22332  mat1dimscm  22362  dmatmul  22384  dmatscmcl  22390  scmataddcl  22403  scmatsubcl  22404  scmatsgrp1  22409  mavmulsolcl  22438  ma1repveval  22458  1marepvmarrepid  22462  symgmatr01lem  22540  slesolvec  22566  cramerimplem2  22571  decpmatmullem  22658  pm2mpf1  22686  mp2pm2mplem4  22696  monmat2matmon  22711  chpscmat  22729  chpscmatgsumbin  22731  fvmptnn04ifb  22738  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  cpmadugsumlemF  22763  toprntopon  22812  clsss  22941  ntrss  22942  restntr  23069  cmpsublem  23286  cmpsub  23287  2ndcrest  23341  txindislem  23520  t0kq  23705  filufint  23807  fbflim2  23864  flftg  23883  alexsubALTlem4  23937  cnextfvval  23952  ustuqtop4  24132  xmettri2  24228  mettri  24240  metss  24396  tngngp3  24544  clmvscom  24990  lmmbr  25158  caublcls  25209  lmcau  25213  ovolunlem1a  25397  nulmbl2  25437  voliunlem1  25451  iunmbl  25454  volsup  25457  dvlip  25898  dvfsumle  25926  dvfsumleOLD  25927  degltlem1  25977  ply1divex  26042  plyco  26146  dgrnznn  26152  dvnply2  26195  plydivex  26205  aannenlem2  26237  aaliou3lem2  26251  ulmcau  26304  zabsle1  27207  gausslemma2dlem1a  27276  gausslemma2dlem2  27278  gausslemma2dlem3  27279  gausslemma2dlem4  27280  2lgslem1a1  27300  2sqnn0  27349  2sqreulem1  27357  2sqreunnlem1  27360  dchrisumlem1  27400  dchrisumlem2  27401  dchrisumlem3  27402  qabvle  27536  ostthlem2  27539  ostth2lem2  27545  nosupbnd1lem5  27624  noinfbnd1lem5  27639  nocvxminlem  27689  nocvxmin  27690  slerec  27731  madebdaylemold  27809  mulsuniflem  28052  precsexlem6  28114  precsexlem7  28115  precsexlem8  28116  precsexlem9  28117  abssge0  28147  noseqind  28186  om2noseqlt  28193  om2noseqrdg  28198  n0addscl  28236  n0mulscl  28237  onsfi  28247  expscllem  28316  tgjustr  28401  axeuclidlem  28889  incistruhgr  29006  umgredgprv  29034  umgrpredgv  29067  usgredgprvALT  29122  uhgr2edg  29135  usgredg2vlem2  29153  lfuhgr1v0e  29181  subgrfun  29208  umgrres1lem  29237  upgrres1  29240  fusgrfis  29257  uhgrnbgr0nb  29281  nbgr1vtx  29285  nb3grprlem1  29307  uvtx01vtx  29324  fusgrn0degnn0  29427  vtxdginducedm1lem4  29470  finsumvtxdg2size  29478  wlkl1loop  29566  wlkres  29598  lfgrwlknloop  29617  pthdadjvtx  29658  dfpth2  29659  upgr2pthnlp  29662  upgrwlkdvdelem  29666  upgrwlkdvde  29667  uhgrwkspthlem2  29684  usgr2trlspth  29691  usgr2pth  29694  pthdlem2lem  29697  cyclnumvtx  29730  lfgrn1cycl  29735  uspgrn2crct  29738  crctcshwlkn0lem3  29742  crctcshwlkn0lem4  29743  crctcshwlkn0lem5  29744  iswspthsnon  29786  wlkiswwlks1  29797  wlklnwwlkln1  29798  wlkiswwlks2  29805  wlkiswwlksupgr2  29807  wlklnwwlkln2lem  29812  wlknwwlksnbij  29818  wwlksnred  29822  wwlksnext  29823  wwlksnredwwlkn  29825  wwlksnredwwlkn0  29826  wwlksnextfun  29828  wwlksnextinj  29829  wwlksnextsurj  29830  wspthsnonn0vne  29847  wspn0  29854  wwlks2onv  29883  elwwlks2  29896  elwspths2spth  29897  rusgrnumwwlk  29905  clwwlkccatlem  29918  clwlkclwwlklem2a1  29921  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2a4  29926  clwlkclwwlklem2a  29927  clwlkclwwlklem2  29929  clwlkclwwlkf1lem3  29935  clwwisshclwwslem  29943  clwwisshclwwsn  29945  erclwwlktr  29951  isclwwlknx  29965  clwwlkinwwlk  29969  clwwlkel  29975  clwwlkf  29976  clwwlkf1  29978  clwwlkfo  29979  clwwlkext2edg  29985  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  clwwlknscsh  29991  erclwwlkntr  30000  eleclclwwlkn  30005  hashecclwwlkn1  30006  umgrhashecclwwlk  30007  clwwlknon0  30022  clwwlknonel  30024  clwwlknon1  30026  clwwlknonwwlknonb  30035  clwwlknonex2lem2  30037  clwwlknun  30041  clwwlkvbij  30042  upgr3v3e3cycl  30109  uhgr3cyclex  30111  upgr4cycl4dv4e  30114  eulerpath  30170  eucrctshift  30172  eucrct2eupth  30174  1to2vfriswmgr  30208  1to3vfriswmgr  30209  3cyclfrgrrn1  30214  4cycl2vnunb  30219  frgrwopreglem2  30242  frgrwopreglem3  30243  frgrwopreglem5ALT  30251  fusgr2wsp2nb  30263  2clwwlk2clwwlklem  30275  2clwwlk2clwwlk  30279  numclwwlk1lem2f1  30286  numclwwlk1lem2fo  30287  numclwwlk1  30290  clwwlknonclwlknonf1o  30291  dlwwlknondlwlknonf1o  30294  numclwlk1  30300  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  numclwwlk5  30317  frgrreg  30323  frgrregord013  30324  friendship  30328  nsnlplig  30410  nsnlpligALT  30411  isgrpo  30426  vcdi  30494  vcdir  30495  vcass  30496  nmosetre  30693  hlim2  31121  shscli  31246  chintcli  31260  dfch2  31336  spansncvi  31581  nmopsetretALT  31792  nmfnsetre  31806  lnopl  31843  lnfnl  31860  pjss2coi  32093  pjorthcoi  32098  pjscji  32099  pjssdif2i  32103  pjclem4a  32127  pj3lem1  32135  strlem5  32184  hstrlem5  32192  cvmdi  32253  mdslmd3i  32261  atcv1  32309  atcvat4i  32326  cdj3lem2a  32365  cdj3lem3a  32368  opreu2reuALT  32406  iuninc  32489  disji2f  32506  disjif2  32510  fmptcof2  32581  xrsmulgzz  32947  ofldchr  33292  1arithufdlem3  33517  esumfzf  34059  issgon  34113  voliune  34219  volfiniune  34220  rrvsum  34445  bnj228  34725  bnj1294  34807  bnj229  34874  bnj607  34906  bnj908  34921  bnj953  34929  bnj1118  34974  bnj1174  34993  bnj1388  35023  funen1cnv  35078  acycgrsubgr  35145  cvmliftlem15  35285  satfsschain  35351  satfdm  35356  satf0op  35364  fmla0xp  35370  gonarlem  35381  goalrlem  35383  satffunlem1lem1  35389  satffunlem2lem1  35391  dmopab3rexdif  35392  satefvfmla0  35405  prv1n  35418  iprodefisumlem  35727  faclimlem1  35730  dfon2lem6  35776  idinside  36072  onsucconni  36425  axc11n11r  36671  bj-brrelex12ALT  37055  bj-snmoore  37101  bj-finsumval0  37273  exlimim  37330  exellim  37332  icoreclin  37345  difunieq  37362  fvineqsneq  37400  pibt2  37405  wl-spae  37509  wl-aleq  37523  fin2so  37601  matunitlindf  37612  poimirlem4  37618  poimirlem26  37640  itg2addnclem  37665  upixp  37723  welb  37730  sdclem2  37736  metf1o  37749  sstotbnd3  37770  isbndx  37776  ismtycnv  37796  heiborlem4  37808  bfplem1  37816  opidonOLD  37846  grpomndo  37869  ax12eq  38934  ax12el  38935  cvrat4  39437  nn0addcom  42450  nn0mulcom  42454  mzpexpmpt  42733  diophren  42801  rmxypos  42936  jm2.17a  42949  jm2.17b  42950  rmygeid  42953  jm2.18  42977  jm2.25  42988  jm2.15nn0  42992  jm2.16nn0  42993  pwslnm  43083  isnumbasgrplem1  43090  dgraalem  43134  onuniintrab  43215  onsupuni  43218  onsupcl3  43222  naddonnn  43384  naddwordnexlem2  43387  relexpiidm  43693  relexpmulnn  43698  relexpmulg  43699  relexp01min  43702  relexp0a  43705  relexpxpmin  43706  clsk1indlem3  44032  grucollcld  44249  dvgrat  44301  radcnvrat  44303  sspwimpcf  44909  sspwimpcfVD  44910  e2ebindALT  44918  trfr  44952  et-sqrtnegnre  46871  fsetprcnexALT  47063  eu2ndop1stv  47126  afvfv0bi  47153  afveu  47154  afvres  47173  aovmpt4g  47202  ndmaovass  47207  ndmaovdistr  47208  afv2orxorb  47229  afv2eu  47239  imarnf1pr  47283  nltle2tri  47314  fzopredsuc  47324  subsubelfzo0  47327  2ffzoeq  47328  2tceilhalfelfzo1  47333  m1modmmod  47359  smonoord  47372  elsetpreimafvssdm  47387  iccpartres  47419  iccpartiltu  47423  iccpartigtl  47424  iccpartgt  47428  icceuelpartlem  47436  fargshiftf1  47442  ichnreuop  47473  ichreuopeq  47474  elsprel  47476  sprsymrelfo  47498  prproropf1olem4  47507  paireqne  47512  sbcpr  47522  reupr  47523  goldbachth  47548  fmtnoprmfac1  47566  fmtnoprmfac2  47568  prmdvdsfmtnof1lem2  47586  lighneallem2  47607  lighneallem4  47611  requad2  47624  even3prm2  47720  fpprwpprb  47741  gbegt5  47762  sbgoldbwt  47778  sbgoldbm  47785  nnsum3primesgbe  47793  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  isubgredg  47866  grimuhgr  47887  clnbgrgrim  47934  grtriprop  47940  cycl3grtrilem  47945  cycl3grtri  47946  gpgusgralem  48047  gpgedgvtx0  48052  gpgedgvtx1  48053  gpgcubic  48070  gpg5nbgr3star  48072  gpgprismgr4cycllem3  48087  upgrwlkupwlk  48128  uspgropssxp  48132  uspgrsprfo  48136  isassintop  48198  lidldomn1  48219  2zlidl  48228  2zrngamgm  48233  2zrngmmgm  48240  rngccatidALTV  48260  rngcinvALTV  48264  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem9  48286  ringccatidALTV  48294  srhmsubcALTV  48313  lmodvsmdi  48367  ply1mulgsumlem1  48375  ply1mulgsumlem2  48376  lincdifsn  48413  lincsumcl  48420  lincscmcl  48421  lincext3  48445  lindslinindsimp1  48446  lindslinindsimp2lem5  48451  snlindsntor  48460  lincresunit2  48467  lincresunit3lem2  48469  zgtp1leeq  48510  elbigo2  48541  fllog2  48557  digexp  48596  dig1  48597  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  1arymaptf1  48631  2arymaptf1  48642  rrxlinec  48725  eenglngeehlnm  48728  rrx2linest  48731  itsclc0yqsol  48753  itsclc0xyqsol  48757