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  1058  19.29r  1878  19.41v  1954  19.41  2229  nfsb4t  2499  mo4  2561  2euexv  2628  2euex  2638  raleqbidvvOLD  3331  gencl  3516  2gencl  3517  vtocl2ga  3567  vtocl4g  3572  rspccva  3612  2reurex  3757  2reu1  3892  rexdifi  4146  sseq0  4400  r19.2z  4495  ralf0  4514  falseral0  4520  elelpwi  4613  preqsnd  4860  prproe  4907  ssuni  4937  disji2  5131  invdisjrab  5135  disjiun  5136  disjxiun  5146  trintss  5285  ssexg  5324  reusv2lem3  5399  propeqop  5508  otiunsndisj  5521  rexopabb  5529  pofun  5607  solin  5614  2optocl  5772  3optocl  5773  ssrelrn  5895  elrnmpt1  5958  resieq  5993  reuop  6293  funimaexgOLD  6636  fnun  6664  fss  6735  fun  6754  fvelimab  6965  fvmptss  7011  fvn0ssdmfun  7077  fvcofneq  7095  fmptco  7127  funsndifnop  7149  fnressn  7156  fressnfv  7158  fvn0fvelrnOLD  7161  fmptsng  7166  fvtp2g  7200  fvtp3g  7201  tpres  7202  fnex  7219  funfvima3  7238  isores3  7332  tfisg  7843  dmfex  7898  opreuopreu  8020  releldmdifi  8031  funeldmdif  8034  el2mpocsbcl  8071  f1o2ndf1  8108  frxp  8112  fnse  8119  frxp2  8130  frxp3  8137  poseq  8144  ressuppssdif  8170  funsssuppss  8175  suppssOLD  8180  mpoxopxnop0  8200  reldmtpos  8219  frrlem8  8278  fpr2a  8287  wfrfunOLD  8319  wfrlem12OLD  8320  smores  8352  tfrlem7  8383  tz7.48-2  8442  tz7.49  8445  oacl  8535  omcl  8536  oecl  8537  oarec  8562  oewordri  8592  oeworde  8593  oelim2  8595  oeoa  8597  oeoelem  8598  oeoe  8599  nnacl  8611  nnmcl  8612  nnecl  8613  nnmsucr  8625  2ecoptocl  8802  fsetprcnex  8856  undifixp  8928  ssctOLD  9052  xpf1o  9139  limensuc  9154  unfi  9172  imafi  9175  en1eqsn  9274  ac6sfi  9287  frfi  9288  difinf  9316  f1dmvrnfibi  9336  f1vrnfibi  9337  suppeqfsuppbi  9377  elfiun  9425  dffi3  9426  infsupprpr  9499  xpwdomg  9580  infdiffi  9653  ttrclselem2  9721  epfrs  9726  frmin  9744  frr2  9755  rankxpsuc  9877  updjud  9929  tskwe  9945  infxpenlem  10008  fseqenlem1  10019  kmlem2  10146  nnadju  10192  cff1  10253  cflim2  10258  sornom  10272  infpssrlem4  10301  fin23lem26  10320  fin23lem30  10337  fin23lem34  10341  isf32lem11  10358  fin67  10390  isfin7-2  10391  fin1a2lem10  10404  axcc2lem  10431  axdc2lem  10443  axdc3lem2  10446  axdc3lem4  10448  axdc4lem  10450  iunfo  10534  tsk0  10758  gruina  10813  grur1a  10814  mulcanenq  10955  reclem2pr  11043  supsrlem  11106  supsr  11107  ax1rid  11156  negf1o  11644  mulgt1  12073  lbreu  12164  nnindd  12232  nnaddcl  12235  nnmulcl  12236  nn0n0n1ge2b  12540  nn0indd  12659  fzind  12660  fnn0ind  12661  uzaddcl  12888  uzinfi  12912  nn01to3  12925  elpq  12959  xmulasslem2  13261  supxrunb1  13298  supxrunb2  13299  infmremnf  13322  infmrp1  13323  uzsubsubfz  13523  elfz0ubfz0  13605  fz0fzdiffz0  13610  elfzmlbp  13612  fzofzim  13679  elfzom1elp1fzo  13699  ssfzo12bi  13727  fzonfzoufzol  13735  elfznelfzob  13738  injresinjlem  13752  injresinj  13753  modaddmodup  13899  modfzo0difsn  13908  modsumfzodifsn  13909  addmodlteq  13911  om2uzlti  13915  fsequb  13940  ssnn0fi  13950  ser1const  14024  expcllem  14038  expeq0  14058  expmordi  14132  expnngt1  14204  faclbnd  14250  hashf1rn  14312  hashgadd  14337  hashunx  14346  hashnn0n0nn  14351  hashgt0elex  14361  hashss  14369  hashfzp1  14391  hashxp  14394  hashmap  14395  hashimarni  14401  seqcoll  14425  hash2exprb  14432  hashge2el2difr  14442  elss2prb  14448  hashdifsnp1  14457  fi1uzind  14458  brfi1indALT  14461  lswlgt0cl  14519  swrdnd  14604  swrdnnn0nd  14606  swrdnd0  14607  swrd0  14608  swrdsbslen  14614  swrdspsleq  14615  pfxsuff1eqwrdeq  14649  swrdswrdlem  14654  swrdswrd  14655  wrd2ind  14673  pfxccatin12lem2a  14677  swrdccatin2  14679  pfxccatin12lem2  14681  pfxccatin12lem3  14682  pfxccatin12  14683  pfxccat3  14684  swrdccat  14685  pfxccat3a  14688  swrdccat3blem  14689  repswswrd  14734  repswrevw  14737  cshwmodn  14745  cshwsublen  14746  cshwidxmod  14753  cshwidxmodr  14754  cshf1  14760  2cshw  14763  cshweqrep  14771  cshw1  14772  2cshwcshw  14776  cshwcshid  14778  cshwcsh2id  14779  wrdlen2i  14893  2swrd2eqwrdeq  14904  wwlktovfo  14909  relexpsucnnl  14977  rtrclreclem3  15007  rtrclreclem4  15008  relexpindlem  15010  r19.29uz  15297  caubnd  15305  sqreu  15307  climshft  15520  climub  15608  climserle  15609  sumss  15670  sumss2  15672  modfsummods  15739  o1fsum  15759  binom  15776  climcndslem1  15795  climcndslem2  15796  cvgrat  15829  clim2prod  15834  prodfn0  15840  prodfrec  15841  ntrivcvgfvn0  15845  fprodn0  15923  fprodmodd  15941  fprodefsum  16038  demoivreALT  16144  ruclem8  16180  dvdsaddre2b  16250  dvdsdivcl  16259  dvdsfac  16269  oddnn02np1  16291  oddge22np1  16292  evennn02n  16293  evennn2n  16294  m1exp1  16319  nn0o  16326  pwp1fsum  16334  flodddiv4  16356  smu01lem  16426  dvdslegcd  16445  gcdneg  16463  dfgcd2  16488  seq1st  16508  alginv  16512  lcmf  16570  lcmftp  16573  lcmfunsnlem2lem2  16576  lcmfunsnlem  16578  lcmfun  16582  ncoprmgcdne1b  16587  coprmproddvdslem  16599  coprmproddvds  16600  cncongr1  16604  prmdvdsexp  16652  prmndvdsfaclt  16662  ncoprmlnprm  16664  fvprmselgcd1  16978  prmgaplem6  16989  prmgaplem7  16990  prmgaplem8  16991  cshwshashlem1  17029  setsstruct2  17107  setsstruct  17109  inveq  17721  catsubcat  17789  initoeu2lem0  17963  initoeu2lem1  17964  funcestrcsetclem8  18099  funcestrcsetclem9  18100  fthestrcsetc  18102  fullestrcsetc  18103  funcsetcestrclem9  18115  fthsetcestrc  18117  fullsetcestrc  18118  lubss  18466  lubel  18467  issstrmgm  18572  mgmb1mgm1  18574  sgrpidmnd  18630  frmdgsum  18743  smndex1mndlem  18790  mgm2nsgrplem3  18801  dfgrp2  18847  cyccom  19080  gaass  19161  gsumwrev  19233  symgextf1lem  19288  symgextf1  19289  fvcosymgeq  19297  gsmsymgreq  19300  symgfixelsi  19303  pmtrprfv3  19322  symggen  19338  pmtrprfval  19355  gsumzres  19777  gsumpr  19823  gsumzunsnd  19824  srgmulgass  20040  srgbinom  20054  0ringnnzr  20302  lmodvsmmulgdi  20507  lmodfopnelem1  20508  rmodislmodlem  20539  cnfldmulg  20977  cnfldexp  20978  psgndiflemB  21153  assamulgscm  21455  gsumply1subr  21756  gsummoncoe1  21828  pf1ind  21874  matmulcell  21947  mat1dimscm  21977  dmatmul  21999  dmatscmcl  22005  scmataddcl  22018  scmatsubcl  22019  scmatsgrp1  22024  mavmulsolcl  22053  ma1repveval  22073  1marepvmarrepid  22077  symgmatr01lem  22155  slesolvec  22181  cramerimplem2  22186  decpmatmullem  22273  pm2mpf1  22301  mp2pm2mplem4  22311  monmat2matmon  22326  chpscmat  22344  chpscmatgsumbin  22346  fvmptnn04ifb  22353  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulgsum  22366  cpmadugsumlemF  22378  toprntopon  22427  clsss  22558  ntrss  22559  restntr  22686  cmpsublem  22903  cmpsub  22904  2ndcrest  22958  txindislem  23137  t0kq  23322  filufint  23424  fbflim2  23481  flftg  23500  alexsubALTlem4  23554  cnextfvval  23569  ustuqtop4  23749  xmettri2  23846  mettri  23858  metss  24017  tngngp3  24173  clmvscom  24606  lmmbr  24775  caublcls  24826  lmcau  24830  ovolunlem1a  25013  nulmbl2  25053  voliunlem1  25067  iunmbl  25070  volsup  25073  dvlip  25510  dvfsumle  25538  degltlem1  25590  ply1divex  25654  plyco  25755  dgrnznn  25761  dvnply2  25800  plydivex  25810  aannenlem2  25842  aaliou3lem2  25856  ulmcau  25907  zabsle1  26799  gausslemma2dlem1a  26868  gausslemma2dlem2  26870  gausslemma2dlem3  26871  gausslemma2dlem4  26872  2lgslem1a1  26892  2sqnn0  26941  2sqreulem1  26949  2sqreunnlem1  26952  dchrisumlem1  26992  dchrisumlem2  26993  dchrisumlem3  26994  qabvle  27128  ostthlem2  27131  ostth2lem2  27137  nosupbnd1lem5  27215  noinfbnd1lem5  27230  nocvxminlem  27279  nocvxmin  27280  slerec  27321  madebdaylemold  27393  mulsuniflem  27607  precsexlem6  27661  precsexlem7  27662  precsexlem8  27663  precsexlem9  27664  tgjustr  27756  axeuclidlem  28251  incistruhgr  28370  umgredgprv  28398  umgrpredgv  28431  usgredgprvALT  28483  uhgr2edg  28496  usgredg2vlem2  28514  lfuhgr1v0e  28542  subgrfun  28569  umgrres1lem  28598  upgrres1  28601  fusgrfis  28618  uhgrnbgr0nb  28642  nbgr1vtx  28646  nb3grprlem1  28668  uvtx01vtx  28685  fusgrn0degnn0  28787  vtxdginducedm1lem4  28830  finsumvtxdg2size  28838  wlkl1loop  28926  wlkres  28958  lfgrwlknloop  28977  pthdadjvtx  29018  upgr2pthnlp  29020  upgrwlkdvdelem  29024  upgrwlkdvde  29025  uhgrwkspthlem2  29042  usgr2trlspth  29049  usgr2pth  29052  pthdlem2lem  29055  lfgrn1cycl  29090  uspgrn2crct  29093  crctcshwlkn0lem3  29097  crctcshwlkn0lem4  29098  crctcshwlkn0lem5  29099  iswspthsnon  29141  wlkiswwlks1  29152  wlklnwwlkln1  29153  wlkiswwlks2  29160  wlkiswwlksupgr2  29162  wlklnwwlkln2lem  29167  wlknwwlksnbij  29173  wwlksnred  29177  wwlksnext  29178  wwlksnredwwlkn  29180  wwlksnredwwlkn0  29181  wwlksnextfun  29183  wwlksnextinj  29184  wwlksnextsurj  29185  wspthsnonn0vne  29202  wspn0  29209  wwlks2onv  29238  elwwlks2  29251  elwspths2spth  29252  rusgrnumwwlk  29260  clwwlkccatlem  29273  clwlkclwwlklem2a1  29276  clwlkclwwlklem2fv2  29280  clwlkclwwlklem2a4  29281  clwlkclwwlklem2a  29282  clwlkclwwlklem2  29284  clwlkclwwlkf1lem3  29290  clwwisshclwwslem  29298  clwwisshclwwsn  29300  erclwwlktr  29306  isclwwlknx  29320  clwwlkinwwlk  29324  clwwlkel  29330  clwwlkf  29331  clwwlkf1  29333  clwwlkfo  29334  clwwlkext2edg  29340  wwlksext2clwwlk  29341  wwlksubclwwlk  29342  clwwlknscsh  29346  erclwwlkntr  29355  eleclclwwlkn  29360  hashecclwwlkn1  29361  umgrhashecclwwlk  29362  clwwlknon0  29377  clwwlknonel  29379  clwwlknon1  29381  clwwlknonwwlknonb  29390  clwwlknonex2lem2  29392  clwwlknun  29396  clwwlkvbij  29397  upgr3v3e3cycl  29464  uhgr3cyclex  29466  upgr4cycl4dv4e  29469  eulerpath  29525  eucrctshift  29527  eucrct2eupth  29529  1to2vfriswmgr  29563  1to3vfriswmgr  29564  3cyclfrgrrn1  29569  4cycl2vnunb  29574  frgrwopreglem2  29597  frgrwopreglem3  29598  frgrwopreglem5ALT  29606  fusgr2wsp2nb  29618  2clwwlk2clwwlklem  29630  2clwwlk2clwwlk  29634  numclwwlk1lem2f1  29641  numclwwlk1lem2fo  29642  numclwwlk1  29645  clwwlknonclwlknonf1o  29646  dlwwlknondlwlknonf1o  29649  numclwlk1  29655  numclwlk2lem2f  29661  numclwlk2lem2f1o  29663  numclwwlk5  29672  frgrreg  29678  frgrregord013  29679  friendship  29683  nsnlplig  29765  nsnlpligALT  29766  isgrpo  29781  vcdi  29849  vcdir  29850  vcass  29851  nmosetre  30048  hlim2  30476  shscli  30601  chintcli  30615  dfch2  30691  spansncvi  30936  nmopsetretALT  31147  nmfnsetre  31161  lnopl  31198  lnfnl  31215  pjss2coi  31448  pjorthcoi  31453  pjscji  31454  pjssdif2i  31458  pjclem4a  31482  pj3lem1  31490  strlem5  31539  hstrlem5  31547  cvmdi  31608  mdslmd3i  31616  atcv1  31664  atcvat4i  31681  cdj3lem2a  31720  cdj3lem3a  31723  opreu2reuALT  31748  iuninc  31823  disji2f  31839  disjif2  31843  fmptcof2  31913  xrsmulgzz  32210  ofldchr  32463  esumfzf  33098  issgon  33152  voliune  33258  volfiniune  33259  rrvsum  33484  bnj228  33777  bnj1294  33859  bnj229  33926  bnj607  33958  bnj908  33973  bnj953  33981  bnj1118  34026  bnj1174  34045  bnj1388  34075  funen1cnv  34122  acycgrsubgr  34180  cvmliftlem15  34320  satfsschain  34386  satfdm  34391  satf0op  34399  fmla0xp  34405  gonarlem  34416  goalrlem  34418  satffunlem1lem1  34424  satffunlem2lem1  34426  dmopab3rexdif  34427  satefvfmla0  34440  prv1n  34453  iprodefisumlem  34741  faclimlem1  34744  dfon2lem6  34791  idinside  35087  gg-dvfsumle  35213  onsucconni  35370  axc11n11r  35609  bj-brrelex12ALT  35996  bj-snmoore  36042  bj-finsumval0  36214  exlimim  36271  exellim  36273  icoreclin  36286  difunieq  36303  fvineqsneq  36341  pibt2  36346  wl-spae  36438  wl-aleq  36452  fin2so  36523  matunitlindf  36534  poimirlem4  36540  poimirlem26  36562  itg2addnclem  36587  upixp  36645  welb  36652  sdclem2  36658  metf1o  36671  sstotbnd3  36692  isbndx  36698  ismtycnv  36718  heiborlem4  36730  bfplem1  36738  opidonOLD  36768  grpomndo  36791  ax12eq  37859  ax12el  37860  cvrat4  38362  nn0addcom  41371  nn0mulcom  41375  mzpexpmpt  41531  diophren  41599  rmxypos  41734  jm2.17a  41747  jm2.17b  41748  rmygeid  41751  jm2.18  41775  jm2.25  41786  jm2.15nn0  41790  jm2.16nn0  41791  pwslnm  41884  isnumbasgrplem1  41891  dgraalem  41935  onuniintrab  42023  onsupuni  42026  onsupcl3  42030  naddonnn  42194  naddwordnexlem2  42197  relexpiidm  42503  relexpmulnn  42508  relexpmulg  42509  relexp01min  42512  relexp0a  42515  relexpxpmin  42516  clsk1indlem3  42842  grucollcld  43067  dvgrat  43119  radcnvrat  43121  sspwimpcf  43729  sspwimpcfVD  43730  e2ebindALT  43738  et-sqrtnegnre  45637  fsetprcnexALT  45820  eu2ndop1stv  45881  afvfv0bi  45908  afveu  45909  afvres  45928  aovmpt4g  45957  ndmaovass  45962  ndmaovdistr  45963  afv2orxorb  45984  afv2eu  45994  imarnf1pr  46038  nltle2tri  46069  fzopredsuc  46079  subsubelfzo0  46082  fzoopth  46083  2ffzoeq  46084  smonoord  46087  elsetpreimafvssdm  46102  iccpartres  46134  iccpartiltu  46138  iccpartigtl  46139  iccpartgt  46143  icceuelpartlem  46151  fargshiftf1  46157  ichnreuop  46188  ichreuopeq  46189  elsprel  46191  sprsymrelfo  46213  prproropf1olem4  46222  paireqne  46227  sbcpr  46237  reupr  46238  goldbachth  46263  fmtnoprmfac1  46281  fmtnoprmfac2  46283  prmdvdsfmtnof1lem2  46301  lighneallem2  46322  lighneallem4  46326  requad2  46339  even3prm2  46435  fpprwpprb  46456  gbegt5  46477  sbgoldbwt  46493  sbgoldbm  46500  nnsum3primesgbe  46508  wtgoldbnnsum4prm  46518  bgoldbnnsum3prm  46520  bgoldbtbndlem2  46522  bgoldbtbndlem3  46523  bgoldbtbndlem4  46524  bgoldbtbnd  46525  isomuspgrlem1  46543  isomuspgrlem2d  46547  upgrwlkupwlk  46566  uspgropssxp  46570  uspgrsprfo  46574  mgmpropd  46593  isassintop  46668  rngqiprngimfo  46834  lidldomn1  46871  2zlidl  46880  2zrngamgm  46885  2zrngmmgm  46892  rnghmsscmap  46920  rnghmsubcsetclem2  46922  rngcinv  46927  rngccatidALTV  46935  rngcinvALTV  46939  funcrngcsetc  46944  funcrngcsetcALT  46945  rhmsscmap  46966  rhmsubcsetclem2  46968  rhmsubcrngclem2  46974  funcringcsetc  46981  funcringcsetcALTV2lem9  46990  ringccatidALTV  46998  srhmsubc  47022  rhmsubclem4  47035  srhmsubcALTV  47040  rhmsubcALTVlem4  47053  lmodvsmdi  47106  ply1mulgsumlem1  47115  ply1mulgsumlem2  47116  lincdifsn  47153  lincsumcl  47160  lincscmcl  47161  lincext3  47185  lindslinindsimp1  47186  lindslinindsimp2lem5  47191  snlindsntor  47200  lincresunit2  47207  lincresunit3lem2  47209  zgtp1leeq  47250  m1modmmod  47255  elbigo2  47286  fllog2  47302  digexp  47341  dig1  47342  nn0sumshdiglemA  47353  nn0sumshdiglemB  47354  1arymaptf1  47376  2arymaptf1  47387  rrxlinec  47470  eenglngeehlnm  47473  rrx2linest  47476  itsclc0yqsol  47498  itsclc0xyqsol  47502