Theorem com12 33

Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 91. Its associated inference is mpi 21. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

Ref	Expression
com12.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
com12	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem com12

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 32	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl11  34  syl5  35  syl6com  38  mpcom  39  syli  40  syl2imc  42  pm2.27  43  syldc  49  pm2.43b  56  syl9r  79  com3r  88  pm2.86i  111  pm2.24  125  con3rr3  156  exptOLD  179  jad  189  pm2.61  194  syl5ibcom  248  syl5ibrcom  250  pm5.501  369  impcom  412  impd  415  expcom  418  expdcom  419  simplbi2com  507  imdistanri  579  syldbl2  854  jaod  872  orel1  901  pm2.62  912  pm2.75  946  pm2.64  956  ccased  1054  dedlem0b  1060  3impd  1367  3expd  1372  mp3an1i  1483  minimp  1651  meredith  1671  19.35  1907  speimfw  1993  equtrr  2052  equeucl  2054  ax12ev2  2216  sbiedw  2349  cbv1v  2368  exsb  2391  cbv1  2434  ax12b  2456  axc11n  2458  dvelimdf  2481  equvel  2488  dfsb1  2513  sbied  2535  dfmoeu  2563  mo3  2592  mo4  2594  2mo  2676  2eu6  2684  exists2  2689  pm2.61dne  3044  rexlimdv  3164  r19.21v  3190  r19.12  3314  2gencl  3497  3gencl  3498  vtocl2ga  3543  vtocl2gaf  3544  vtocl3gaf  3545  vtocl3ga  3546  vtocl4ga  3548  rspccv  3579  ceqex  3612  mob  3681  euind  3688  reuind  3717  2reu1  3852  sseq2  3964  nelss  4004  rexdifi  4105  reupick2  4285  disjeq0  4417  uneqdifeq  4454  sspw  4574  ssprsseq  4792  preq12b  4816  prnebg  4822  prel12g  4830  3elpr2eq  4872  iinss2  5023  trintss  5238  dtruALT2  5343  reusv2lem1  5371  alxfr  5380  ralxfrALT  5388  exexneq  5418  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  snopeqop  5491  propeqop  5492  opthhausdorff  5502  opthhausdorff0  5503  pofun  5589  solin  5598  frss  5627  2optocl  5759  3optocl  5760  ssrel  5771  ssrel2  5773  ssrelrel  5784  relop  5838  dfres3  5985  asymref2  6119  xpidtr  6124  trin2  6125  poltletr  6134  xp11  6175  imadifssranOLD  6205  relcnvtrg  6270  reuop  6296  tz7.7  6388  ordtr2  6408  suc11  6472  fundif  6587  fss  6724  f0dom0  6764  fv3  6901  tz6.12i  6909  mpteqb  7011  fveqdmss  7075  eldmrexrnb  7089  funopsnOLD  7147  funsndifnop  7150  tpres  7201  funfvima  7230  fvclss  7241  f1veqaeq  7256  fvf1pr  7307  isoselem  7341  oprabv  7472  ovg  7577  elovmpt3rab1  7672  sorpsscmpl  7733  iunpw  7771  trom  7872  limom  7879  peano5  7891  focdmex  7954  funelss  8045  funeldmdif  8046  bropopvvv  8086  bropfvvvvlem  8087  f1o2ndf1  8118  poxp  8125  soxp  8126  poxp2  8140  frxp2  8141  frxp3  8148  suppimacnv  8171  ressuppss  8180  ressuppssdif  8182  tposfn2  8245  wfr3g  8317  onnseq  8332  smoel  8348  smogt  8355  smoiso2  8357  tfr3  8387  tz7.48-2  8430  tz7.48-3  8432  tz7.49  8433  oecl  8523  oaordex  8544  oalimcl  8546  oaass  8547  omordi  8552  omlimcl  8564  odi  8565  omeulem1  8568  oen0  8573  nnawordi  8608  nnaass  8609  nnmordi  8618  omabs  8638  omsmolem  8644  naddssim  8673  brinxper  8725  iiner  8788  2ecoptocl  8807  3ecoptocl  8808  undifixp  8933  xpdom2  9061  xpf1o  9128  infensuc  9144  findcard2  9150  php  9192  isinf  9226  unblem2  9254  fodomfir  9288  infssuni  9304  finsschain  9317  fsuppunfi  9349  fsuppunbi  9350  marypha1  9395  hartogs  9507  card2on  9517  card2inf  9518  xpwdomg  9548  elirrvOLD  9561  elirrvOLDOLD  9562  en3lp  9584  preleqg  9585  inf3lem1  9598  inf3lem2  9599  inf3lem3  9600  inf3lem5  9602  noinfep  9630  ttrclss  9690  ttrclselem2  9696  trcl  9698  tcel  9713  frr3g  9729  rankonidlem  9801  scottex  9860  djuunxp  9908  eldju2ndl  9911  updjud  9921  dif1card  9995  fodomnum  10042  cardaleph  10074  kmlem9  10143  kmlem13  10147  cflim2  10248  cfsmolem  10255  infpssrlem3  10290  isfin7-2  10381  fin1a2lem6  10390  fin1a2lem12  10396  domtriomlem  10427  axdc3lem4  10438  axdc4lem  10440  zorn2lem3  10483  zorn2lem4  10484  zorn2lem5  10485  zorn2lem7  10487  zornn0g  10490  axdclem2  10505  ondomon  10548  alephval2  10558  cfpwsdom  10570  wuncval2  10733  grupr  10783  gruiun  10785  ingru  10801  grothomex  10815  indpi  10893  nqereu  10915  prlem934  11019  reclem2pr  11034  mulgt0sr  11091  supsrlem  11097  1re  11209  dedekind  11374  lemul1a  12070  squeeze0  12119  peano5nni  12237  nnadddir  12293  nnunb  12501  nn0lt2  12660  nn0le2is012  12661  fzind  12695  nn0ind-raph  12697  zindd  12698  uzin  12899  nn01to3  12966  xnn0xadd0  13274  xmulasslem  13312  icoshft  13501  fzen  13570  uzsubsubfz  13576  elfz0ubfz0  13662  elfz0fzfz0  13663  fz0fzelfz0  13664  elfzmlbp  13669  elfzodifsumelfzo  13762  ssfzo12bi  13792  fzoopth  13793  elfzonelfzo  13800  elfznelfzo  13804  injresinjlem  13821  injresinj  13822  modfzo0difsn  13981  modsumfzodifsn  13982  addmodlteq  13984  ssnn0fi  14023  fsuppmapnn0fiub0  14031  expcllem  14110  expeq0  14130  mulexp  14139  leexp2r  14212  bernneq  14267  facdiv  14325  hasheqf1oi  14389  hashnn0n0nn  14429  hashss  14447  hashgt12el  14461  hashgt12el2  14462  hashimarni  14480  hashle2pr  14516  pr2pwpr  14518  hashge2el2dif  14519  hashge2el2difr  14520  hashtpg  14524  hashge3el3dif  14526  exprelprel  14529  hash1to3  14531  hash3tpde  14532  tpfo  14539  fundmge2nop0  14541  fi1uzind  14546  ccatsymb  14622  swrdnd  14694  swrdnd2  14695  swrdnnn0nd  14696  swrdnd0  14697  pfxnd0  14728  swrdswrdlem  14743  swrdswrd  14744  pfxccatin12lem2a  14766  pfxccatin12lem1  14767  swrdccatin2  14768  pfxccatin12lem2  14770  pfxccatin12lem3  14771  pfxccat3  14773  swrdccat  14774  swrdccat3blem  14778  repsdf2  14817  repswswrd  14823  cshwidxmod  14842  cshwidx0  14845  cshf1  14849  cshweqrep  14860  cshw1  14861  2cshwcshw  14864  scshwfzeqfzo  14865  cshwcsh2id  14867  wwlktovfo  14997  relexpaddg  15092  iseraltlem2  15736  modfsummods  15847  clim2prod  15944  prodfn0  15950  prodfrec  15951  prodmo  15992  fprodabs  16030  binomfallfac  16096  fprodefsum  16150  dvdsaddre2b  16366  addmodlteqALT  16384  oddge22np1  16408  nn0enne  16436  nn0o1gt2  16440  sumeven  16446  sumodd  16447  dvdslegcd  16563  gcdneg  16581  dfgcd2  16605  rplpwr  16617  lcmf  16692  lcmftp  16695  lcmfunsnlem2lem1  16697  lcmfunsnlem2  16699  lcmfdvdsb  16702  coprmdvds1  16711  qredeq  16716  coprmprod  16720  coprmproddvdslem  16721  cncongr1  16726  cncongr2  16727  prm2orodd  16750  2mulprm  16752  nnnn0modprm0  16867  prm23lt5  16875  prm23ge5  16876  dvdsprmpweqnn  16946  dvdsprmpweqle  16947  oddprmdvds  16964  prmpwdvds  16965  prmreclem4  16980  ramcl  17090  prmgaplem6  17117  prmgaplem7  17118  prmgaplem8  17119  cshwshashlem1  17156  cshwshashlem2  17157  cshwshashlem3  17158  cshwrepswhash1  17163  setsn0fun  17234  setsstruct2  17235  imasleval  17596  mreiincl  17649  mreexexd  17705  inveq  17832  cicsym  17862  cictr  17863  initoid  18059  termoid  18060  initoeu2lem0  18071  initoeu2lem1  18072  initoeu2lem2  18073  initoeu2  18074  fthestrcsetc  18207  fthsetcestrc  18222  drsdirfi  18362  isnmgm  18703  mgmhmlin  18758  issubmgm2  18762  sgrpass  18784  insubm  18878  mgm2nsgrplem3  18983  dfgrp3lem  19105  cyccom  19275  symg2bas  19464  symgfix2  19487  symgextf1  19492  gsmsymgrfix  19499  pmtrprfv3  19525  psgnunilem4  19568  efgi2  19796  0ringnnzr  20610  rnghmsscmap  20716  rnghmsubcsetclem2  20718  rngcinv  20723  funcrngcsetc  20726  funcrngcsetcALT  20727  rhmsscmap  20745  rhmsubcsetclem2  20747  rhmsubcrngclem2  20753  ringcbasbas  20759  funcringcsetc  20760  rhmsubclem4  20774  unichnlidl  21343  rngqiprngimfo  21422  psgndiflemB  21731  psgndiflemA  21732  elfrlmbasn0  21894  lmictra  21976  mpfrcl  22217  gsummoncoe1  22449  mamufacex  22534  matecl  22563  dmatelnd  22634  dmatscmcl  22641  scmateALT  22650  scmatsgrp1  22660  scmatf1  22669  mavmulsolcl  22689  cramerimplem1  22821  cramerimplem2  22822  pmatcollpw3fi1  22926  mp2pm2mplem4  22947  pm2mpfo  22952  chmaidscmat  22986  fvmptnn04ifb  22989  chfacfscmul0  22996  chfacfpmmul0  23000  cayhamlem1  23004  cayhamlem3  23025  cayleyhamilton1  23030  fiinopn  23039  tgcl  23107  distop  23133  isclo2  23226  iscldtop  23233  ssnei2  23254  opnnei  23258  pnfnei  23358  mnfnei  23359  tgcnp  23391  cnpnei  23402  1stcelcls  23599  txcnpi  23746  cnmptcom  23816  fbfinnfr  23979  isfildlem  23995  snfil  24002  fbunfip  24007  fgcl  24016  elfm2  24086  fmco  24099  fbflim2  24115  cnpflf2  24138  flimfcls  24164  tmdgsum  24233  neibl  24639  tngngpim  24797  fgcfil  25411  caubl  25448  volsuplem  25695  ellimc3  26019  dvnadd  26069  dvnres  26071  cpnord  26075  dvnfre  26092  ply1divex  26275  cxpmul2  26832  fsumdvdsmul  27337  zabsle1  27438  gausslemma2dlem1a  27507  gausslemma2dlem3  27510  lgsquad2lem2  27527  2lgs  27549  2sq2  27575  2sqnn0  27580  2sqnn  27581  2sqreultlem  27589  2sqreunnltlem  27592  qabvexp  27768  ltsval2  27798  nolt02o  27837  sltsun1  27959  cutsun12  27961  madebday  28071  mulsprop  28301  precsexlem8  28385  precsexlem9  28386  noseqind  28463  om2noseqrdg  28475  n0cutlt  28530  peano5uzs  28575  expadds  28606  bdaypw2n0bndlem  28634  bdaypw2n0bnd  28635  axcontlem4  29295  umgredgprv  29435  umgrnloop  29436  upgrpredgv  29467  upgredgpr  29470  edglnl  29471  usgredgprvALT  29523  usgrnloopALT  29531  usgredg2v  29555  fusgrfis  29658  nbuhgr2vtx1edgblem  29679  nb3grprlem1  29708  cusgrsize2inds  29781  cusgrfi  29786  fusgrn0degnn0  29827  uspgrloopvtxel  29844  vtxdginducedm1lem4  29870  uhgr0edg0rgrb  29902  wlkl1loop  29965  wlk1walk  29966  upgriswlk  29968  upgrwlkvtxedg  29972  uspgr2wlkeq  29973  wlkv0  29977  wlksoneq1eq2  29990  wlkon2n0  29992  wlkreslem  29995  wlkres  29996  lfgrwlkprop  30013  pthdivtx  30054  2pthnloop  30058  spthonepeq  30079  uhgrwkspthlem2  30081  uhgrwkspth  30082  usgr2wlkneq  30083  usgr2trlncl  30087  usgr2pthlem  30090  usgr2pth  30091  cyclnspth  30128  lfgrn1cycl  30132  usgr2trlncrct  30133  uspgrn2crct  30135  crctcshwlkn0lem3  30139  crctcshwlkn0lem5  30141  wwlknp  30170  wspthneq1eq2  30187  0enwwlksnge1  30191  wlklnwwlkln1  30195  wlkiswwlks2  30202  wlkiswwlksupgr2  30204  wlklnwwlkln2lem  30209  wwlksnred  30219  wwlksnextbi  30221  wwlksnredwwlkn0  30223  wwlksnextwrd  30224  wwlksnextinj  30226  wwlksnextproplem3  30238  wwlksnextprop  30239  wspthsnwspthsnon  30243  wspthsnonn0vne  30244  2pthon3v  30270  umgr2adedgwlkonALT  30274  umgr2wlk  30276  umgr2wlkon  30277  usgrwwlks2on  30285  umgrwwlks2on  30286  elwspths2on  30289  elwspths2onw  30290  usgr2wspthons3  30294  elwwlks2  30296  rusgrnumwwlk  30305  clwwlkccatlem  30318  clwlkclwwlklem2a4  30326  clwlkclwwlklem2a  30327  clwlkclwwlklem2  30329  clwlkclwwlkf1lem3  30335  erclwwlkeqlen  30348  clwwlknwwlksn  30367  loopclwwlkn1b  30371  clwwlkf1  30378  wwlksext2clwwlk  30386  eleclclwwlknlem2  30390  umgr2cwwk2dif  30393  eleclclwwlkn  30405  hashecclwwlkn1  30406  umgrhashecclwwlk  30407  clwwlknonwwlknonb  30435  clwwlknonex2lem2  30437  clwwlknonex2  30438  1pthon2v  30482  upgr3v3e3cycl  30509  uhgr3cyclexlem  30510  uhgr3cyclex  30511  eupth2lem3lem4  30560  frgr3vlem1  30602  frgr3vlem2  30603  3vfriswmgrlem  30606  3vfriswmgr  30607  3cyclfrgrrn1  30614  n4cyclfrgr  30620  frgrncvvdeqlem3  30630  frgrncvvdeqlem6  30633  frgrncvvdeqlem7  30634  frgrncvvdeqlem8  30635  frgrwopreglem4a  30639  frgrwopreglem3  30643  frgrwopreg1  30647  frgrwopreg2  30648  frgrwopreglem5lem  30649  frgrwopreglem5ALT  30651  frgrwopreg  30652  fusgr2wsp2nb  30663  2wspmdisj  30666  numclwwlk1lem2foa  30683  numclwwlk1lem2f1  30686  numclwwlk1lem2fo  30687  numclwwlk1  30690  wlkl0  30696  numclwwlk2lem1  30705  numclwlk2lem2f  30706  numclwlk2lem2f1o  30708  frgrreg  30723  frgrregord013  30724  frgrregord13  30725  friendshipgt3  30727  friendship  30728  eulplig  30815  ipassi  31171  ubthlem2  31201  isch3  31571  shintcli  31659  shmodsi  31719  spansncvi  31982  hoaddsub  32146  eigorthi  32167  pjss2coi  32494  pjnormssi  32498  pj3cor1i  32539  strb  32588  dmdmd  32630  mdsl0  32640  csmdsymi  32664  chrelat2i  32695  mdsymlem3  32735  mdsymlem6  32738  sumdmdlem2  32749  opreu2reuALT  32801  ssrelf  32938  gsumwun  33374  r1filim  35476  trssfir1om  35485  fineqvinfep  35516  trssfir1omregs  35527  karddom  35552  kardsdom  35553  kardexen  35554  onvf1odlem4  35568  spthcycl  35599  loop1cycl  35607  cvmlift2lem1  35772  satfrel  35837  satfrnmapom  35840  fmlafvel  35855  fmla1  35857  gonarlem  35864  gonar  35865  goalrlem  35866  goalr  35867  satffunlem  35871  satffunlem1lem1  35872  satffunlem2lem1  35874  satffun  35879  satefvfmla1  35895  mrsubvrs  35992  mclsax  36039  3ccased  36189  dfon2lem3  36253  rdgprc  36262  cgrextend  36478  btwndiff  36497  btwnconn1lem12  36568  brsegle  36578  broutsideof2  36592  funray  36610  in-ax8  36714  ss-ax8  36715  elicc3  36806  nn0prpwlem  36811  nn0prpw  36812  fnessref  36846  neibastop2lem  36849  filnetlem4  36870  meran1  36900  waj-ax  36903  arg-ax  36905  axtco1from2  36964  dfttc4  37019  mh-inf3f1  37030  mh-regprimbi  37034  bj-nnclavc  37114  bj-con2com  37131  bj-axdd2  37163  bj-alrimg  37184  bj-exlimg  37206  bj-exalimi  37216  bj-eximcom  37217  bj-ssbid1ALT  37265  bj-sb  37290  bj-snsetex  37577  bj-axseprep  37689  bj-axreprepsep  37690  bj-restpw  37712  bj-finsumval0  37907  mptsnunlem  37962  icoreclin  37981  relowlpssretop  37988  inunissunidif  37999  rdgssun  38002  finorwe  38006  domalom  38028  wl-dral1d  38164  wl-exeq  38167  wl-lem-exsb  38199  wl-eujustlem1  38221  poimirlem29  38278  poimirlem32  38281  fdc  38374  seqpo  38376  incsequz  38377  isismty  38430  ismtybndlem  38435  heibor1lem  38438  ismgmOLD  38479  isexid2  38484  ghomco  38520  pridlc  38700  relcnveq3  38954  elrelscnveq3  39254  cdleme18d  41047  tendovalco  41517  cdlemn11pre  41962  dihord2pre  41977  indstrd  42938  unitscyglem3  42942  eu6w  43388  incssnn0  43422  fphpd  43523  jm2.19lem3  43698  setindtr  43731  islssfg2  43778  mpaaeu  43857  ordnexbtwnsuc  43974  oaabsb  44001  succlg  44035  oacl2g  44037  omabs2  44039  omcl2  44040  omcl3g  44041  pr2cv  44254  refimssco  44313  iunrelexpmin1  44414  iunrelexpmin2  44418  trclimalb2  44432  clsk1indlem3  44749  tfindsd  44914  mnurndlem1  44971  nzss  45007  sb5ALT  45214  truniALT  45230  ee223  45323  3orbi123VD  45538  sbc3orgVD  45539  exbirVD  45541  exbiriVD  45542  sbcim2gVD  45563  trsbcVD  45565  truniALTVD  45566  onfrALTlem3VD  45575  onfrALTlem2VD  45577  csbrngVD  45584  19.41rgVD  45590  ax6e2eqVD  45595  ax6e2ndeqVD  45597  2uasbanhVD  45599  sb5ALTVD  45601  vk15.4jVD  45602  infxrunb3rnmpt  46122  stoweidlem26  46720  et-equeucl  47566  hirstL-ax3  47606  rexsb  47813  rexrsb  47814  euoreqb  47823  2reu8i  47827  afvres  47886  tz6.12-afv  47887  afvco2  47890  afv2orxorb  47942  afv2res  47953  tz6.12-afv2  47954  tz6.12i-afv2  47957  dfatcolem  47969  zm1nn  48016  2ffzoeq  48042  smonoord  48091  iccpartiltu  48148  iccpartlt  48150  iccpartltu  48151  iccpartgtl  48152  iccpartgt  48153  iccpartleu  48154  iccpartgel  48155  icceuelpart  48162  iccpartnel  48164  lswn0  48170  ichnreuop  48198  ichreuopeq  48199  prsprel  48213  sprsymrelfvlem  48216  sprsymrelf1lem  48217  sprsymrelfolem2  48219  prproropf1olem4  48232  paireqne  48237  prprelb  48242  reupr  48248  goldbachth  48276  odz2prm2pw  48292  fmtno4prmfac  48301  fmtno4prmfac193  48302  prmdvdsfmtnof1lem2  48314  2pwp1prmfmtno  48319  lighneallem2  48335  lighneallem4b  48338  lighneallem4  48339  requad2  48365  odd2prm2  48460  mogoldbblem  48462  gbepos  48500  gbowgt5  48504  gbowge7  48505  stgoldbwt  48518  sbgoldbwt  48519  sbgoldbst  48520  sbgoldbaltlem1  48521  sbgoldbalt  48523  sbgoldbo  48529  nnsum3primesle9  48536  nnsum4primesodd  48538  nnsum4primesoddALTV  48539  nnsum4primeseven  48542  nnsum4primesevenALTV  48543  bgoldbtbndlem1  48547  bgoldbtbndlem2  48548  bgoldbtbndlem3  48549  bgoldbtbnd  48551  dfnbgr6  48599  isuspgrimlem  48637  uhgrimisgrgric  48673  clnbgrgrim  48676  usgrgrtrirex  48692  isubgr3stgrlem4  48711  grilcbri2  48753  grlicsym  48755  grlictr  48757  gricgrlic  48760  gpgvtxedg0  48805  gpgvtxedg1  48806  gpgedg2ov  48808  gpgedg2iv  48809  pgnioedg1  48850  pgnioedg2  48851  pgnioedg3  48852  pgnioedg4  48853  pgnioedg5  48854  pgnbgreunbgrlem2lem3  48858  pgnbgreunbgrlem3  48860  pgnbgreunbgrlem5lem1  48862  pgnbgreunbgrlem5lem2  48863  pgnbgreunbgrlem5lem3  48864  pgnbgreunbgrlem6  48866  upgrwlkupwlk  48882  uspgrsprf1  48889  lmod0rng  48971  lidldomn1  48973  rngccatidALTV  49014  rngcinvALTV  49018  rhmsubcALTVlem4  49026  funcringcsetcALTV2lem9  49040  ringccatidALTV  49048  ringcbasbasALTV  49054  ztprmneprm  49104  pgrpgt2nabl  49123  lmodvsmdi  49136  ply1mulgsumlem2  49144  lincsumcl  49188  ellcoellss  49192  linindslinci  49205  islinindfis  49206  lincext3  49213  lindslinindimp2lem4  49218  lindslinindsimp2lem5  49219  lindslinindsimp2  49220  lindsrng01  49225  ldepspr  49230  lincresunit3lem1  49236  elfzolborelfzop1  49276  dignn0ldlem  49359  nn0sumshdiglem1  49378  1arymaptf1  49399  2arymaptf1  49410  rrx2xpref1o  49475  rrx2plord2  49479  rrx2plordisom  49480  line2ylem  49508  line2xlem  49510  line2y  49512  itschlc0xyqsol1  49523  inlinecirc02plem  49543  fullthinc  50205  tfis2d  50435  onsetrec  50463