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  1059  19.29r  1876  19.41v  1951  19.41  2243  nfsb4t  2504  mo4  2567  2euexv  2632  2euex  2642  gencl  3472  2gencl  3473  vtocl2ga  3522  vtocl2gaf  3523  vtocl3gaf  3525  vtocl3ga  3527  vtocl4g  3529  vtocl4ga  3530  rspccva  3564  2reurex  3707  2reu1  3836  rexdifi  4091  sseq0  4344  r19.2z  4440  falseral0OLD  4456  elelpwi  4552  preqsnd  4803  prproe  4849  ssuni  4876  disji2  5070  disjiun  5074  disjxiun  5083  trintss  5211  ssexg  5260  reusv2lem3  5337  propeqop  5455  otiunsndisj  5468  rexopabb  5476  pofun  5550  solin  5559  2optocl  5720  3optocl  5721  ssrelrn  5843  elrnmpt1  5909  resieq  5949  imadifssran  6109  reuop  6251  fnun  6606  fss  6678  fun  6696  fvelimab  6906  fvmptss  6954  fvn0ssdmfun  7020  fvcofneq  7039  fmptco  7076  funsndifnop  7098  fnressn  7105  fressnfv  7107  fmptsng  7116  fvtp2g  7147  fvtp3g  7148  tpres  7149  fnex  7165  funfvima3  7184  fvf1pr  7255  isores3  7283  tfisg  7798  dmfex  7849  opreuopreu  7980  releldmdifi  7991  funeldmdif  7994  el2mpocsbcl  8028  f1o2ndf1  8065  frxp  8069  fnse  8076  frxp2  8087  frxp3  8094  poseq  8101  ressuppssdif  8128  funsssuppss  8133  mpoxopxnop0  8158  reldmtpos  8177  frrlem8  8236  fpr2a  8245  smores  8285  tfrlem7  8315  tz7.48-2  8374  tz7.49  8377  oacl  8463  omcl  8464  oecl  8465  oarec  8490  oewordri  8521  oeworde  8522  oelim2  8524  oeoa  8526  oeoelem  8527  oeoe  8528  nnacl  8540  nnmcl  8541  nnecl  8542  nnmsucr  8554  naddoa  8631  brinxper  8666  2ecoptocl  8748  fsetprcnex  8802  undifixp  8875  xpf1o  9070  limensuc  9085  unfi  9098  en1eqsn  9178  ac6sfi  9187  frfi  9188  difinf  9214  imafiOLD  9219  f1dmvrnfibi  9244  f1vrnfibi  9245  suppeqfsuppbi  9285  elfiun  9336  dffi3  9337  infsupprpr  9412  xpwdomg  9493  infdiffi  9570  ttrclselem2  9638  epfrs  9643  frmin  9664  frr2  9675  rankxpsuc  9797  updjud  9849  tskwe  9865  infxpenlem  9926  fseqenlem1  9937  kmlem2  10065  nnadju  10111  cff1  10171  cflim2  10176  sornom  10190  infpssrlem4  10219  fin23lem26  10238  fin23lem30  10255  fin23lem34  10259  isf32lem11  10276  fin67  10308  isfin7-2  10309  fin1a2lem10  10322  axcc2lem  10349  axdc2lem  10361  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  iunfo  10452  tsk0  10677  gruina  10732  grur1a  10733  mulcanenq  10874  reclem2pr  10962  supsrlem  11025  supsr  11026  ax1rid  11075  negf1o  11571  mulgt1OLD  12005  lbreu  12097  nnindd  12185  nnaddcl  12188  nnmulcl  12189  nn0n0n1ge2b  12497  nn0indd  12617  fzind  12618  fnn0ind  12619  uzaddcl  12845  uzinfi  12869  nn01to3  12882  elpq  12916  xmulasslem2  13225  supxrunb1  13262  supxrunb2  13263  infmremnf  13287  infmrp1  13288  uzsubsubfz  13491  fzdif1  13550  elfz0ubfz0  13577  fz0fzdiffz0  13582  elfzmlbp  13584  fzofzim  13655  elfzom1elp1fzo  13678  ssfzo12bi  13707  fzoopth  13708  fzonfzoufzol  13717  elfznelfzob  13720  injresinjlem  13736  injresinj  13737  modaddmodup  13887  modfzo0difsn  13896  modsumfzodifsn  13897  addmodlteq  13899  om2uzlti  13903  fsequb  13928  ssnn0fi  13938  ser1const  14011  expcllem  14025  expeq0  14045  expmordi  14120  expnngt1  14194  faclbnd  14243  hashf1rn  14305  hashgadd  14330  hashunx  14339  hashnn0n0nn  14344  hashgt0elex  14354  hashss  14362  hashfzp1  14384  hashxp  14387  hashmap  14388  hashimarni  14394  seqcoll  14417  hash2exprb  14424  hashge2el2difr  14434  elss2prb  14441  hashdifsnp1  14459  fi1uzind  14460  brfi1indALT  14463  lswlgt0cl  14522  swrdnd  14608  swrdnnn0nd  14610  swrdnd0  14611  swrd0  14612  swrdsbslen  14618  swrdspsleq  14619  pfxsuff1eqwrdeq  14652  swrdswrdlem  14657  swrdswrd  14658  wrd2ind  14676  pfxccatin12lem2a  14680  swrdccatin2  14682  pfxccatin12lem2  14684  pfxccatin12lem3  14685  pfxccatin12  14686  pfxccat3  14687  swrdccat  14688  pfxccat3a  14691  swrdccat3blem  14692  repswswrd  14737  repswrevw  14740  cshwmodn  14748  cshwsublen  14749  cshwidxmod  14756  cshwidxmodr  14757  cshf1  14763  2cshw  14766  cshweqrep  14774  cshw1  14775  2cshwcshw  14778  cshwcshid  14780  cshwcsh2id  14781  wrdlen2i  14895  2swrd2eqwrdeq  14906  wwlktovfo  14911  relexpsucnnl  14983  rtrclreclem3  15013  rtrclreclem4  15014  relexpindlem  15016  r19.29uz  15304  caubnd  15312  sqreu  15314  climshft  15529  climub  15615  climserle  15616  sumss  15677  sumss2  15679  modfsummods  15747  o1fsum  15767  binom  15786  climcndslem1  15805  climcndslem2  15806  cvgrat  15839  clim2prod  15844  prodfn0  15850  prodfrec  15851  ntrivcvgfvn0  15855  fprodn0  15935  fprodmodd  15953  fprodefsum  16051  demoivreALT  16159  ruclem8  16195  dvdsaddre2b  16267  dvdsdivcl  16276  dvdsfac  16286  oddnn02np1  16308  oddge22np1  16309  evennn02n  16310  evennn2n  16311  m1exp1  16336  nn0o  16343  pwp1fsum  16351  flodddiv4  16375  smu01lem  16445  dvdslegcd  16464  gcdneg  16482  dfgcd2  16506  seq1st  16531  alginv  16535  lcmf  16593  lcmftp  16596  lcmfunsnlem2lem2  16599  lcmfunsnlem  16601  lcmfun  16605  ncoprmgcdne1b  16610  coprmproddvdslem  16622  coprmproddvds  16623  cncongr1  16627  prmdvdsexp  16676  prmndvdsfaclt  16686  ncoprmlnprm  16689  fvprmselgcd1  17007  prmgaplem6  17018  prmgaplem7  17019  prmgaplem8  17020  cshwshashlem1  17057  setsstruct2  17135  setsstruct  17137  inveq  17732  catsubcat  17797  initoeu2lem0  17971  initoeu2lem1  17972  funcestrcsetclem8  18104  funcestrcsetclem9  18105  fthestrcsetc  18107  fullestrcsetc  18108  funcsetcestrclem9  18120  fthsetcestrc  18122  fullsetcestrc  18123  lubss  18470  lubel  18471  mgmpropd  18610  issstrmgm  18612  mgmb1mgm1  18614  sgrpidmnd  18698  frmdgsum  18821  smndex1mndlem  18871  mgm2nsgrplem3  18882  dfgrp2  18929  cyccom  19169  gaass  19263  gsumwrev  19332  symgextf1lem  19386  symgextf1  19387  fvcosymgeq  19395  gsmsymgreq  19398  symgfixelsi  19401  pmtrprfv3  19420  symggen  19436  pmtrprfval  19453  gsumzres  19875  gsumpr  19921  gsumzunsnd  19922  srgmulgass  20189  srgbinom  20203  0ringnnzr  20493  rnghmsscmap  20598  rnghmsubcsetclem2  20600  rngcinv  20605  funcrngcsetc  20608  funcrngcsetcALT  20609  rhmsscmap  20627  rhmsubcsetclem2  20629  rhmsubcrngclem2  20635  funcringcsetc  20642  srhmsubc  20648  rhmsubclem4  20656  lmodvsmmulgdi  20883  lmodfopnelem1  20884  rmodislmodlem  20915  rngqiprngimfo  21291  cnfldmulg  21393  cnfldexp  21394  ofldchr  21566  psgndiflemB  21590  assamulgscm  21891  gsumply1subr  22207  gsummoncoe1  22283  pf1ind  22330  matmulcell  22420  mat1dimscm  22450  dmatmul  22472  dmatscmcl  22478  scmataddcl  22491  scmatsubcl  22492  scmatsgrp1  22497  mavmulsolcl  22526  ma1repveval  22546  1marepvmarrepid  22550  symgmatr01lem  22628  slesolvec  22654  cramerimplem2  22659  decpmatmullem  22746  pm2mpf1  22774  mp2pm2mplem4  22784  monmat2matmon  22799  chpscmat  22817  chpscmatgsumbin  22819  fvmptnn04ifb  22826  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulgsum  22839  cpmadugsumlemF  22851  toprntopon  22900  clsss  23029  ntrss  23030  restntr  23157  cmpsublem  23374  cmpsub  23375  2ndcrest  23429  txindislem  23608  t0kq  23793  filufint  23895  fbflim2  23952  flftg  23971  alexsubALTlem4  24025  cnextfvval  24040  ustuqtop4  24219  xmettri2  24315  mettri  24327  metss  24483  tngngp3  24631  clmvscom  25067  lmmbr  25235  caublcls  25286  lmcau  25290  ovolunlem1a  25473  nulmbl2  25513  voliunlem1  25527  iunmbl  25530  volsup  25533  dvlip  25970  dvfsumle  25998  degltlem1  26047  ply1divex  26112  plyco  26216  dgrnznn  26222  dvnply2  26264  plydivex  26274  aannenlem2  26306  aaliou3lem2  26320  ulmcau  26373  zabsle1  27273  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  gausslemma2dlem3  27345  gausslemma2dlem4  27346  2lgslem1a1  27366  2sqnn0  27415  2sqreulem1  27423  2sqreunnlem1  27426  dchrisumlem1  27466  dchrisumlem2  27467  dchrisumlem3  27468  qabvle  27602  ostthlem2  27605  ostth2lem2  27611  nosupbnd1lem5  27690  noinfbnd1lem5  27705  nocvxminlem  27760  lesrec  27805  madebdaylemold  27904  mulsuniflem  28155  precsexlem6  28218  precsexlem7  28219  precsexlem8  28220  precsexlem9  28221  abssge0  28251  noseqind  28298  om2noseqlt  28305  om2noseqrdg  28310  n0addscl  28350  n0mulscl  28351  onsfi  28362  oldfib  28383  expscllem  28436  pw2cut2  28468  z12zsodd  28488  tgjustr  28556  axeuclidlem  29045  incistruhgr  29162  umgredgprv  29190  umgrpredgv  29223  usgredgprvALT  29278  uhgr2edg  29291  usgredg2vlem2  29309  lfuhgr1v0e  29337  subgrfun  29364  umgrres1lem  29393  upgrres1  29396  fusgrfis  29413  uhgrnbgr0nb  29437  nbgr1vtx  29441  nb3grprlem1  29463  uvtx01vtx  29480  fusgrn0degnn0  29583  vtxdginducedm1lem4  29626  finsumvtxdg2size  29634  wlkl1loop  29721  wlkres  29752  lfgrwlknloop  29771  pthdadjvtx  29811  dfpth2  29812  upgr2pthnlp  29815  upgrwlkdvdelem  29819  upgrwlkdvde  29820  uhgrwkspthlem2  29837  usgr2trlspth  29844  usgr2pth  29847  pthdlem2lem  29850  cyclnumvtx  29883  lfgrn1cycl  29888  uspgrn2crct  29891  crctcshwlkn0lem3  29895  crctcshwlkn0lem4  29896  crctcshwlkn0lem5  29897  iswspthsnon  29939  wlkiswwlks1  29950  wlklnwwlkln1  29951  wlkiswwlks2  29958  wlkiswwlksupgr2  29960  wlklnwwlkln2lem  29965  wlknwwlksnbij  29971  wwlksnred  29975  wwlksnext  29976  wwlksnredwwlkn  29978  wwlksnredwwlkn0  29979  wwlksnextfun  29981  wwlksnextinj  29982  wwlksnextsurj  29983  wspthsnonn0vne  30000  wspn0  30007  wwlks2onv  30036  elwwlks2  30052  elwspths2spth  30053  rusgrnumwwlk  30061  clwwlkccatlem  30074  clwlkclwwlklem2a1  30077  clwlkclwwlklem2fv2  30081  clwlkclwwlklem2a4  30082  clwlkclwwlklem2a  30083  clwlkclwwlklem2  30085  clwlkclwwlkf1lem3  30091  clwwisshclwwslem  30099  clwwisshclwwsn  30101  erclwwlktr  30107  isclwwlknx  30121  clwwlkinwwlk  30125  clwwlkel  30131  clwwlkf  30132  clwwlkf1  30134  clwwlkfo  30135  clwwlkext2edg  30141  wwlksext2clwwlk  30142  wwlksubclwwlk  30143  clwwlknscsh  30147  erclwwlkntr  30156  eleclclwwlkn  30161  hashecclwwlkn1  30162  umgrhashecclwwlk  30163  clwwlknon0  30178  clwwlknonel  30180  clwwlknon1  30182  clwwlknonwwlknonb  30191  clwwlknonex2lem2  30193  clwwlknun  30197  clwwlkvbij  30198  upgr3v3e3cycl  30265  uhgr3cyclex  30267  upgr4cycl4dv4e  30270  eulerpath  30326  eucrctshift  30328  eucrct2eupth  30330  1to2vfriswmgr  30364  1to3vfriswmgr  30365  3cyclfrgrrn1  30370  4cycl2vnunb  30375  frgrwopreglem2  30398  frgrwopreglem3  30399  frgrwopreglem5ALT  30407  fusgr2wsp2nb  30419  2clwwlk2clwwlklem  30431  2clwwlk2clwwlk  30435  numclwwlk1lem2f1  30442  numclwwlk1lem2fo  30443  numclwwlk1  30446  clwwlknonclwlknonf1o  30447  dlwwlknondlwlknonf1o  30450  numclwlk1  30456  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  numclwwlk5  30473  frgrreg  30479  frgrregord013  30480  friendship  30484  nsnlplig  30567  nsnlpligALT  30568  isgrpo  30583  vcdi  30651  vcdir  30652  vcass  30653  nmosetre  30850  hlim2  31278  shscli  31403  chintcli  31417  dfch2  31493  spansncvi  31738  nmopsetretALT  31949  nmfnsetre  31963  lnopl  32000  lnfnl  32017  pjss2coi  32250  pjorthcoi  32255  pjscji  32256  pjssdif2i  32260  pjclem4a  32284  pj3lem1  32292  strlem5  32341  hstrlem5  32349  cvmdi  32410  mdslmd3i  32418  atcv1  32466  atcvat4i  32483  cdj3lem2a  32522  cdj3lem3a  32525  opreu2reuALT  32561  iuninc  32645  disji2f  32662  disjif2  32666  fmptcof2  32745  xrsmulgzz  33084  1arithufdlem3  33621  esumfzf  34229  issgon  34283  voliune  34389  volfiniune  34390  rrvsum  34614  bnj228  34894  bnj1294  34975  bnj229  35042  bnj607  35074  bnj908  35089  bnj953  35097  bnj1118  35142  bnj1174  35161  bnj1388  35191  funen1cnv  35247  rankfilimbi  35260  r1filimi  35262  trssfir1om  35271  trssfir1omregs  35296  acycgrsubgr  35356  cvmliftlem15  35496  satfsschain  35562  satfdm  35567  satf0op  35575  fmla0xp  35581  gonarlem  35592  goalrlem  35594  satffunlem1lem1  35600  satffunlem2lem1  35602  dmopab3rexdif  35603  satefvfmla0  35616  prv1n  35629  iprodefisumlem  35938  faclimlem1  35941  dfon2lem6  35984  idinside  36282  onsucconni  36635  axuntco  36677  ttcmin  36694  elttctr  36703  dfttc2g  36704  mh-inf3f1  36739  bj-cbvew  36952  axc11n11r  36996  bj-brrelex12ALT  37390  bj-snmoore  37441  bj-finsumval0  37615  exlimim  37672  exellim  37674  icoreclin  37687  difunieq  37704  fvineqsneq  37742  pibt2  37747  wl-spae  37860  wl-aleq  37874  fin2so  37942  matunitlindf  37953  poimirlem4  37959  poimirlem26  37981  itg2addnclem  38006  upixp  38064  welb  38071  sdclem2  38077  metf1o  38090  sstotbnd3  38111  isbndx  38117  ismtycnv  38137  heiborlem4  38149  bfplem1  38157  opidonOLD  38187  grpomndo  38210  eldisjdmqsim2  39151  ax12eq  39401  ax12el  39402  cvrat4  39903  nn0addcom  42921  nn0mulcom  42925  mzpexpmpt  43191  diophren  43259  rmxypos  43393  jm2.17a  43406  jm2.17b  43407  rmygeid  43410  jm2.18  43434  jm2.25  43445  jm2.15nn0  43449  jm2.16nn0  43450  pwslnm  43540  isnumbasgrplem1  43547  dgraalem  43591  onuniintrab  43672  onsupuni  43675  onsupcl3  43679  naddonnn  43841  naddwordnexlem2  43844  relexpiidm  44149  relexpmulnn  44154  relexpmulg  44155  relexp01min  44158  relexp0a  44161  relexpxpmin  44162  clsk1indlem3  44488  grucollcld  44705  dvgrat  44757  radcnvrat  44759  sspwimpcf  45364  sspwimpcfVD  45365  e2ebindALT  45373  trfr  45407  et-sqrtnegnre  47319  fsetprcnexALT  47522  eu2ndop1stv  47585  afvfv0bi  47612  afveu  47613  afvres  47632  aovmpt4g  47661  ndmaovass  47666  ndmaovdistr  47667  afv2orxorb  47688  afv2eu  47698  imarnf1pr  47742  nltle2tri  47773  fzopredsuc  47784  subsubelfzo0  47787  2ffzoeq  47788  2tceilhalfelfzo1  47796  m1modmmod  47824  smonoord  47837  elsetpreimafvssdm  47858  iccpartres  47890  iccpartiltu  47894  iccpartigtl  47895  iccpartgt  47899  icceuelpartlem  47907  fargshiftf1  47913  ichnreuop  47944  ichreuopeq  47945  elsprel  47947  sprsymrelfo  47969  prproropf1olem4  47978  paireqne  47983  sbcpr  47993  reupr  47994  goldbachth  48022  fmtnoprmfac1  48040  fmtnoprmfac2  48042  prmdvdsfmtnof1lem2  48060  lighneallem2  48081  lighneallem4  48085  requad2  48111  even3prm2  48207  fpprwpprb  48228  gbegt5  48249  sbgoldbwt  48265  sbgoldbm  48272  nnsum3primesgbe  48280  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbndlem4  48296  bgoldbtbnd  48297  isubgredg  48354  grimuhgr  48375  clnbgrgrim  48422  grtriprop  48429  cycl3grtrilem  48434  cycl3grtri  48435  gpgusgralem  48544  gpgedgvtx0  48549  gpgedgvtx1  48550  gpgcubic  48567  gpg5nbgr3star  48569  gpgprismgr4cycllem3  48585  upgrwlkupwlk  48628  uspgropssxp  48632  uspgrsprfo  48636  isassintop  48698  lidldomn1  48719  2zlidl  48728  2zrngamgm  48733  2zrngmmgm  48740  rngccatidALTV  48760  rngcinvALTV  48764  rhmsubcALTVlem4  48772  funcringcsetcALTV2lem9  48786  ringccatidALTV  48794  srhmsubcALTV  48813  lmodvsmdi  48867  ply1mulgsumlem1  48874  ply1mulgsumlem2  48875  lincdifsn  48912  lincsumcl  48919  lincscmcl  48920  lincext3  48944  lindslinindsimp1  48945  lindslinindsimp2lem5  48950  snlindsntor  48959  lincresunit2  48966  lincresunit3lem2  48968  zgtp1leeq  49009  elbigo2  49040  fllog2  49056  digexp  49095  dig1  49096  nn0sumshdiglemA  49107  nn0sumshdiglemB  49108  1arymaptf1  49130  2arymaptf1  49141  rrxlinec  49224  eenglngeehlnm  49227  rrx2linest  49230  itsclc0yqsol  49252  itsclc0xyqsol  49256