Theorem impcom 396

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

Syntax hints:   → wi 4   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  mpan9  498  bianir  1074  19.29r  1967  19.41v  2042  19.41vOLD  2095  19.41  2273  nfsb4t  2550  2euex  2708  gencl  3428  2gencl  3429  vtocl4g  3469  rspccva  3500  sseq0  4170  r19.2z  4252  falseral0  4271  elelpwi  4361  preqsnd  4575  prproe  4624  ssuni  4650  disji2  4824  invdisjrab  4827  disjiun  4828  disjxiun  4837  trintss  4958  ssexg  4996  reusv2lem3  5066  propeqop  5159  otiunsndisj  5172  pofun  5245  solin  5252  2optocl  5395  3optocl  5396  ssrelrn  5513  elrnmpt1  5572  resieq  5608  funimaexg  6183  fnun  6205  fss  6266  fun  6278  fvelimab  6471  fvmptss  6510  fvn0ssdmfun  6569  fvcofneq  6586  fmptco  6616  funsndifnop  6637  fnressn  6646  fressnfv  6648  fvn0fvelrn  6651  fmptsng  6656  fvtp2g  6686  fvtp3g  6687  tpres  6688  fnex  6703  funfvima3  6717  isores3  6806  dmfex  7351  el2mpt2csbcl  7480  f1o2ndf1  7516  frxp  7518  fnse  7525  ressuppssdif  7547  funsssuppss  7553  suppss  7557  mpt2xopxnop0  7573  reldmtpos  7592  wfrfun  7658  wfrlem12  7659  smores  7682  tfrlem7  7712  tz7.48-2  7770  tz7.49  7773  oacl  7849  omcl  7850  oecl  7851  oarec  7876  oewordri  7906  oeworde  7907  oelim2  7909  oeoa  7911  oeoelem  7912  oeoe  7913  nnacl  7925  nnmcl  7926  nnecl  7927  nnmsucr  7939  2ecoptocl  8070  undifixp  8178  ssct  8277  xpf1o  8358  limensuc  8373  ac6sfi  8440  frfi  8441  difinf  8466  f1dmvrnfibi  8486  f1vrnfibi  8487  suppeqfsuppbi  8525  elfiun  8572  dffi3  8573  xpwdomg  8726  preleqOLD  8758  infdiffi  8799  epfrs  8851  rankxpsuc  8989  updjud  9040  tskwe  9056  infxpenlem  9116  fseqenlem1  9127  kmlem2  9255  cff1  9362  cflim2  9367  sornom  9381  infpssrlem4  9410  fin23lem26  9429  fin23lem30  9446  fin23lem34  9450  isf32lem11  9467  fin67  9499  isfin7-2  9500  fin1a2lem10  9513  axcc2lem  9540  axdc2lem  9552  axdc3lem2  9555  axdc3lem4  9557  axdc4lem  9559  iunfo  9643  tsk0  9867  gruina  9922  grur1a  9923  mulcanenq  10064  reclem2pr  10152  supsrlem  10214  supsr  10215  ax1rid  10264  negf1o  10742  mulgt1  11164  fiminre  11254  lbreu  11255  nnaddcl  11324  nnmulcl  11325  nn0n0n1ge2b  11621  nn0indd  11736  fzind  11737  fnn0ind  11738  uzaddcl  11958  uzinfi  11983  nn01to3  11996  xmulasslem2  12326  supxrunb1  12363  supxrunb2  12364  infmremnf  12387  infmrp1  12388  uzsubsubfz  12582  elfz0ubfz0  12663  fz0fzdiffz0  12668  elfzmlbp  12670  fzofzim  12735  elfzom1elp1fzo  12755  elfzom1p1elfzo  12768  ssfzo12bi  12783  fzonfzoufzol  12791  elfznelfzob  12794  injresinjlem  12808  injresinj  12809  modaddmodup  12953  modfzo0difsn  12962  modsumfzodifsn  12963  addmodlteq  12965  om2uzlti  12969  fsequb  12994  ssnn0fi  13004  ser1const  13076  expcllem  13090  expeq0  13109  faclbnd  13293  faclbnd6  13302  hashf1rn  13357  hashgadd  13380  hashunx  13389  hashnn0n0nn  13394  hashgt0elex  13402  hashss  13410  hashfzp1  13431  hashxp  13434  hashmap  13435  hashimarni  13441  seqcoll  13461  hash2exprb  13466  hashge2el2difr  13476  elss2prb  13482  hashdifsnp1  13491  fi1uzind  13492  brfi1indALT  13495  lswlgt0cl  13564  ccat1st1st  13622  swrdnd  13652  swrd0  13654  swrdsbslen  13668  swrdspsleq  13669  2swrd1eqwrdeq  13674  swrdswrdlem  13679  swrdswrd  13680  wrd2ind  13697  swrdccatfn  13702  swrdccatin1  13703  swrdccatin12lem2a  13705  swrdccatin2  13707  swrdccatin12lem2  13709  swrdccatin12lem3  13710  swrdccatin12  13711  swrdccat3  13712  swrdccat  13713  swrdccat3blem  13715  repswswrd  13751  repswrevw  13753  cshwmodn  13761  cshwsublen  13762  cshwidxmod  13769  cshwidxmodr  13770  cshf1  13776  2cshw  13779  cshweqrep  13787  cshw1  13788  2cshwcshw  13791  cshwcshid  13793  cshwcsh2id  13794  wrdlen2i  13907  2swrd2eqwrdeq  13917  wwlktovfo  13922  relexpsucnnl  13991  rtrclreclem3  14019  rtrclreclem4  14020  relexpindlem  14022  cjexp  14109  absexp  14263  r19.29uz  14309  caubnd  14317  sqreu  14319  climshft  14526  climub  14611  climserle  14612  sumss  14674  sumss2  14676  modfsummods  14743  o1fsum  14763  binom  14780  bcxmas  14785  climcndslem1  14799  climcndslem2  14800  pwm1geoser  14818  cvgrat  14832  clim2prod  14837  prodfn0  14843  prodfrec  14844  ntrivcvgfvn0  14848  fprodn0  14926  fprodmodd  14944  fprodefsum  15041  demoivreALT  15147  znnenlemOLD  15156  ruclem8  15182  dvdsaddre2b  15248  dvdsdivcl  15257  dvdsfac  15267  oddnn02np1  15288  oddge22np1  15289  evennn02n  15290  evennn2n  15291  m1exp1  15309  nn0o  15315  pwp1fsum  15330  flodddiv4  15352  smu01lem  15422  dvdslegcd  15441  gcdneg  15458  dfgcd2  15478  gcdmultiple  15484  seq1st  15499  alginv  15503  lcmf  15561  lcmftp  15564  lcmfunsnlem2lem2  15567  lcmfunsnlem  15569  lcmfun  15573  ncoprmgcdne1b  15578  coprmproddvdslem  15590  coprmproddvds  15591  cncongr1  15595  prmdvdsexp  15640  prmndvdsfaclt  15648  ncoprmlnprm  15649  fvprmselgcd1  15962  prmgaplem6  15973  prmgaplem7  15974  prmgaplem8  15975  cshwshashlem1  16010  setsstruct2  16103  setsstruct  16105  inveq  16634  catsubcat  16699  initoeu2lem0  16863  initoeu2lem1  16864  funcestrcsetclem8  16988  funcestrcsetclem9  16989  fthestrcsetc  16991  fullestrcsetc  16992  funcsetcestrclem9  17004  fthsetcestrc  17006  fullsetcestrc  17007  lubss  17322  lubel  17323  issstrmgm  17453  mgmb1mgm1  17455  frmdgsum  17600  mgm2nsgrplem3  17608  dfgrp2  17648  gaass  17927  gsumwrev  17993  symgextf1lem  18037  symgextf1  18038  fvcosymgeq  18046  gsmsymgreq  18049  symgfixelsi  18052  pmtrprfv3  18071  symggen  18087  pmtrprfval  18104  gsumzres  18507  gsumzunsnd  18552  srgmulgass  18729  srgbinom  18743  lmodvsmmulgdi  19098  lmodfopnelem1  19099  rmodislmodlem  19130  0ringnnzr  19474  assamulgscm  19555  gsumply1subr  19808  gsummoncoe1  19878  pf1ind  19923  cnfldmulg  19982  cnfldexp  19983  psgndiflemB  20150  matmulcell  20457  matmulcellOLD  20458  mat1dimscm  20488  dmatmul  20510  dmatscmcl  20516  scmataddcl  20529  scmatsubcl  20530  scmatsgrp1  20535  mavmulsolcl  20564  ma1repveval  20584  1marepvmarrepid  20588  symgmatr01lem  20667  slesolvec  20693  cramerimplem2  20699  decpmatmullem  20785  pm2mpf1  20813  mp2pm2mplem4  20823  monmat2matmon  20838  chpscmat  20856  chpscmatgsumbin  20858  fvmptnn04ifb  20865  chfacfscmul0  20872  chfacfscmulgsum  20874  chfacfpmmul0  20876  chfacfpmmulgsum  20878  cpmadugsumlemF  20890  clsss  21068  ntrss  21069  restntr  21196  cmpsublem  21412  cmpsub  21413  2ndcrest  21467  txindislem  21646  t0kq  21831  filufint  21933  fbflim2  21990  flftg  22009  alexsubALTlem4  22063  cnextfvval  22078  tmdmulg  22105  ustuqtop4  22257  xmettri2  22354  mettri  22366  metss  22522  tngngp3  22669  clmvscom  23098  lmmbr  23264  caublcls  23315  lmcau  23319  ovolunlem1a  23473  nulmbl2  23513  voliunlem1  23527  iunmbl  23530  volsup  23533  dvlip  23966  dvfsumle  23994  degltlem1  24042  ply1divex  24106  plyco  24207  dgrnznn  24213  dvnply2  24252  plydivex  24262  aannenlem2  24294  aaliou3lem2  24308  ulmcau  24359  zabsle1  25231  gausslemma2dlem1a  25300  gausslemma2dlem2  25302  gausslemma2dlem3  25303  gausslemma2dlem4  25304  2lgslem1a1  25324  dchrisumlem1  25388  dchrisumlem2  25389  dchrisumlem3  25390  qabvle  25524  ostthlem2  25527  ostth2lem2  25533  axeuclidlem  26052  incistruhgr  26184  umgredgprv  26212  umgrpredgv  26246  usgredgprvALT  26298  uhgr2edg  26311  usgredg2vlem2  26329  lfuhgr1v0e  26358  subgrfun  26385  umgrres1lem  26414  upgrres1  26417  fusgrfis  26434  uhgrnbgr0nb  26462  nbgr1vtx  26466  nb3grprlem1  26494  uvtx01vtx  26514  uvtxa01vtx0OLD  26516  fusgrn0degnn0  26619  vtxdginducedm1lem4  26662  finsumvtxdg2size  26670  upgrewlkle2  26726  wlkl1loop  26758  wlkres  26791  lfgrwlknloop  26810  pthdadjvtx  26850  upgr2pthnlp  26852  upgrwlkdvdelem  26856  upgrwlkdvde  26857  uhgrwkspthlem2  26874  usgr2trlspth  26881  usgr2pth  26884  pthdlem2lem  26887  lfgrn1cycl  26922  uspgrn2crct  26925  crctcshwlkn0lem3  26929  crctcshwlkn0lem4  26930  crctcshwlkn0lem5  26931  iswspthsnon  26975  wlkiswwlks1  26990  wlklnwwlkln1  26991  wlkiswwlks2  26998  wlkiswwlksupgr2  27000  wlklnwwlkln2lem  27005  wlknwwlksnbij  27015  wwlksnred  27025  wwlksnext  27026  wwlksnredwwlkn  27028  wwlksnredwwlkn0  27029  wwlksnextfun  27031  wwlksnextinj  27032  wwlksnextsur  27033  wspthsnonn0vne  27053  wspn0  27060  wwlks2onv  27089  elwwlks2  27104  elwspths2spth  27105  rusgrnumwwlk  27113  clwwlknclwwlkdifsOLD  27118  clwwlkccatlem  27128  clwlkclwwlklem2a1  27131  clwlkclwwlklem2fv2  27135  clwlkclwwlklem2a4  27136  clwlkclwwlklem2a  27137  clwlkclwwlklem2  27139  clwlkclwwlkf1lem3  27145  clwwisshclwwslem  27153  clwwisshclwwsn  27155  erclwwlktr  27161  isclwwlknx  27180  clwwlkinwwlk  27185  clwwlkel  27191  clwwlkf  27192  clwwlkf1  27194  clwwlkfo  27195  clwwlkext2edg  27202  wwlksext2clwwlk  27203  wwlksext2clwwlkOLD  27204  wwlksubclwwlk  27205  clwwlknscsh  27209  erclwwlkntr  27218  eleclclwwlkn  27223  hashecclwwlkn1  27224  umgrhashecclwwlk  27225  clwlksfclwwlkOLD  27232  clwlksfoclwwlkOLD  27233  clwwlknon0  27256  clwwlknonel  27258  clwwlknon1  27261  clwwlknonwwlknonb  27270  clwwlknonwwlknonbOLD  27271  clwwlknonex2lem2  27273  clwwlknun  27277  clwwlkvbij  27278  clwwlkvbijOLDOLD  27279  clwwlkvbijOLD  27280  clwwlknunOLD  27282  upgr3v3e3cycl  27349  uhgr3cyclex  27351  upgr4cycl4dv4e  27354  eulerpath  27410  eucrctshift  27412  eucrct2eupth  27414  1to2vfriswmgr  27450  1to3vfriswmgr  27451  3cyclfrgrrn1  27456  4cycl2vnunb  27461  frgrwopreglem2  27484  frgrwopreglem3  27485  frgrwopreglem5ALT  27493  fusgr2wsp2nb  27505  numclwwlk2lem1lemOLD  27515  2clwwlk2clwwlklem  27519  2clwwlk2clwwlk  27523  numclwwlk1lem2f1  27532  numclwwlk1lem2fo  27533  numclwwlk1  27537  clwwlknonclwlknonf1o  27538  dlwwlknondlwlknonf1o  27541  numclwlk1  27547  numclwlk2lem2f  27553  numclwlk2lem2f1o  27555  numclwlk2lem2fOLD  27560  numclwlk2lem2f1oOLD  27562  numclwwlk5  27572  frgrreg  27578  frgrregord013  27579  friendship  27583  nsnlplig  27660  nsnlpligALT  27661  isgrpo  27676  vcdi  27745  vcdir  27746  vcass  27747  nmosetre  27944  hlim2  28374  shscli  28501  chintcli  28515  dfch2  28591  spansncvi  28836  nmopsetretALT  29047  nmfnsetre  29061  lnopl  29098  lnfnl  29115  pjss2coi  29348  pjorthcoi  29353  pjscji  29354  pjssdif2i  29358  pjclem4a  29382  pj3lem1  29390  strlem5  29439  hstrlem5  29447  cvmdi  29508  mdslmd3i  29516  atcv1  29564  atcvat4i  29581  cdj3lem2a  29620  cdj3lem3a  29623  iuninc  29701  disji2f  29712  disjif2  29716  fmptcof2  29781  nnindd  29890  xrsmulgzz  30000  ofldchr  30136  esumfzf  30453  issgon  30508  voliune  30614  volfiniune  30615  rrvsum  30838  bnj228  31123  bnj1294  31208  bnj229  31274  bnj607  31306  bnj908  31321  bnj953  31329  bnj1118  31372  bnj1174  31391  bnj1388  31421  cvmliftlem15  31600  iprodefisumlem  31945  faclimlem1  31948  dfon2lem6  32010  tfisg  32033  poseq  32071  frrlem5c  32104  noprefixmo  32166  nosupbnd1lem5  32176  nocvxminlem  32211  nocvxmin  32212  slerec  32241  idinside  32509  nn0prpw  32636  onsucconni  32750  axc11n11r  32985  bj-finsumval0  33461  exlimim  33503  exellim  33505  icoreclin  33518  wl-spae  33619  wl-aleq  33633  fin2so  33706  matunitlindf  33717  poimirlem4  33723  poimirlem26  33745  itg2addnclem  33770  upixp  33833  welb  33840  sdclem2  33846  metf1o  33859  sstotbnd3  33883  isbndx  33889  ismtycnv  33909  heiborlem4  33921  bfplem1  33929  opidonOLD  33959  grpomndo  33982  ax12eq  34717  ax12el  34718  cvrat4  35220  mzpexpmpt  37807  diophren  37876  expmordi  38010  rmxypos  38012  jm2.17a  38025  jm2.17b  38026  rmygeid  38029  jm2.18  38053  jm2.25  38064  jm2.15nn0  38068  jm2.16nn0  38069  pwslnm  38162  isnumbasgrplem1  38169  dgraalem  38213  relexpiidm  38493  relexpmulnn  38498  relexpmulg  38499  relexp01min  38502  relexp0a  38505  relexpxpmin  38506  clsk1indlem3  38838  dvgrat  39008  radcnvrat  39010  sspwimpcf  39647  sspwimpcfVD  39648  e2ebindALT  39656  2reurex  41690  2reu1  41695  eu2ndop1stv  41711  afvfv0bi  41738  afveu  41739  afvres  41758  aovmpt4g  41787  ndmaovass  41792  ndmaovdistr  41793  afv2orxorb  41814  afv2eu  41824  imarnf1pr  41869  nltle2tri  41895  fzopredsuc  41905  subsubelfzo0  41908  fzoopth  41909  2ffzoeq  41910  smonoord  41913  iccpartres  41926  iccpartiltu  41930  iccpartigtl  41931  iccpartgt  41935  icceuelpartlem  41943  fargshiftf1  41949  pfxsuff1eqwrdeq  41979  pfxccatin12lem2  41996  pfxccatin12  41997  pfxccat3  41998  pfxccat3a  42001  cshword2  42009  goldbachth  42031  fmtnoprmfac1  42049  fmtnoprmfac2  42051  prmdvdsfmtnof1lem2  42069  lighneallem2  42095  lighneallem4  42099  even3prm2  42200  gbegt5  42221  sbgoldbwt  42237  sbgoldbm  42244  nnsum3primesgbe  42252  wtgoldbnnsum4prm  42262  bgoldbnnsum3prm  42264  bgoldbtbndlem2  42266  bgoldbtbndlem3  42267  bgoldbtbndlem4  42268  bgoldbtbnd  42269  upgrwlkupwlk  42286  elsprel  42290  sprsymrelfo  42312  uspgropssxp  42317  uspgrsprfo  42321  mgmpropd  42340  isassintop  42411  lidldomn1  42486  lidlmmgm  42490  2zlidl  42499  2zrngamgm  42504  2zrngmmgm  42511  rnghmsscmap  42539  rnghmsubcsetclem2  42541  rngcinv  42546  rngccatidALTV  42554  rngcinvALTV  42558  funcrngcsetc  42563  funcrngcsetcALT  42564  rhmsscmap  42585  rhmsubcsetclem2  42587  rhmsubcrngclem2  42593  ringcinv  42597  funcringcsetc  42600  funcringcsetcALTV2lem9  42609  ringccatidALTV  42617  ringcinvALTV  42621  srhmsubc  42641  rhmsubclem4  42654  srhmsubcALTV  42659  rhmsubcALTVlem4  42672  gsumpr  42704  lmodvsmdi  42728  ply1mulgsumlem1  42739  ply1mulgsumlem2  42740  lincdifsn  42778  lincsumcl  42785  lincscmcl  42786  lincext3  42810  lindslinindsimp1  42811  lindslinindsimp2lem5  42816  snlindsntor  42825  lincresunit2  42832  lincresunit3lem2  42834  lincresunit3  42835  zgtp1leeq  42876  m1modmmod  42881  elbigo2  42911  fllog2  42927  digexp  42966  dig1  42967  nn0sumshdiglemA  42978  nn0sumshdiglemB  42979