Theorem com12 32

Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 90. Its associated inference is mpi 20. (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 22	. 2 ⊢ (𝜓 → 𝜓)
2		com12.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5com 31	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  33  syl5  34  syl6com  37  mpcom  38  syli  39  syl2imc  41  pm2.27  42  syldc  48  pm2.43b  55  syl9r  78  com3r  87  pm2.86i  110  pm2.24  124  con3rr3  155  expt  177  jad  187  pm2.61  191  syl5ibcom  244  syl5ibrcom  246  pm5.501  367  impcom  408  impd  411  expcom  414  expdcom  415  simplbi2com  503  imdistanri  570  syldbl2  838  jaod  856  orel1  886  pm2.62  897  pm2.75  931  pm2.64  939  ccased  1036  dedlem0b  1042  3impd  1347  3expd  1352  mp3an1i  1453  norassOLD  1536  minimp  1624  meredith  1644  19.35  1881  speimfw  1968  equtrr  2026  equeucl  2028  sbiedw  2311  cbv1v  2334  exsb  2358  cbv1  2403  ax12b  2425  axc11n  2427  dvelimdf  2450  equvel  2457  dfsb1  2486  sbied  2508  dfmoeu  2537  mo3  2565  mo4  2567  2mo  2651  2eu6  2659  exists2  2664  pm2.61dne  3032  r19.21v  3114  rexlimdv  3213  r19.12  3258  r19.12OLD  3259  2gencl  3473  3gencl  3474  vtocl2ga  3515  rspccv  3559  ceqex  3583  mob  3653  euind  3660  reuind  3689  2reu1  3831  sseq2  3948  nelss  3985  rexdifi  4081  reupick2  4255  rspn0OLD  4288  disjeq0  4390  uneqdifeq  4424  sspw  4547  ssprsseq  4759  preq12b  4782  prnebg  4787  prel12g  4795  3elpr2eq  4839  iinss2  4988  trintss  5209  dtruALT2  5294  reusv2lem1  5322  alxfr  5331  ralxfrALT  5339  dtru  5360  copsexgw  5405  copsexg  5406  snopeqop  5421  propeqop  5422  opthhausdorff  5432  opthhausdorff0  5433  poclOLD  5512  pofun  5522  solin  5529  frss  5557  2optocl  5683  3optocl  5684  ssrel  5694  ssrelOLD  5695  ssrel2  5697  ssrelrel  5708  relop  5762  dfres3  5899  asymref2  6027  xpidtr  6032  trin2  6033  poltletr  6042  xp11  6083  relcnvtrg  6174  reuop  6200  tz7.7  6296  ordtr2  6314  suc11  6373  iotaval  6411  funmoOLD  6457  fundif  6490  fss  6626  f0dom0  6667  fv3  6801  tz6.12i  6809  mpteqb  6903  fveqdmss  6965  eldmrexrnb  6977  funopsn  7029  funsndifnop  7032  tpres  7085  funfvima  7115  fvclss  7124  f1veqaeq  7139  isoselem  7221  oprabv  7344  ovg  7446  elovmpt3rab1  7538  sorpsscmpl  7596  iunpw  7630  trom  7730  limom  7737  peano5  7749  peano5OLD  7750  fornex  7807  funelss  7897  funeldmdif  7898  bropopvvv  7939  bropfvvvvlem  7940  f1o2ndf1  7972  poxp  7978  soxp  7979  suppimacnv  7999  ressuppss  8008  ressuppssdif  8010  tposfn2  8073  wfr3g  8147  onnseq  8184  smoel  8200  smogt  8207  smoiso2  8209  tfr3  8239  tz7.48-2  8282  tz7.48-3  8284  tz7.49  8285  oecl  8376  oaordex  8398  oalimcl  8400  oaass  8401  omordi  8406  omlimcl  8418  odi  8419  omeulem1  8422  oen0  8426  nnawordi  8461  nnaass  8462  nnmordi  8471  omabs  8490  omsmolem  8496  iiner  8587  2ecoptocl  8606  3ecoptocl  8607  undifixp  8731  xpdom2  8863  xpf1o  8935  infensuc  8951  findcard2  8956  php  9002  phpOLD  9014  onomeneqOLD  9021  isinf  9045  findcard2OLD  9065  unblem2  9076  infssuni  9119  finsschain  9135  fsuppunfi  9157  fsuppunbi  9158  marypha1  9202  hartogs  9312  card2on  9322  card2inf  9323  xpwdomg  9353  elirrv  9364  en3lp  9381  preleqg  9382  inf3lem1  9395  inf3lem2  9396  inf3lem3  9397  inf3lem5  9399  noinfep  9427  ttrclss  9487  ttrclselem2  9493  trcl  9495  tcel  9512  frr3g  9523  rankonidlem  9595  scottex  9652  djuunxp  9688  eldju2ndl  9691  updjud  9701  dif1card  9775  fodomnum  9822  cardaleph  9854  kmlem9  9923  kmlem13  9927  cflim2  10028  cfsmolem  10035  infpssrlem3  10070  isfin7-2  10161  fin1a2lem6  10170  fin1a2lem12  10176  domtriomlem  10207  axdc3lem4  10218  axdc4lem  10220  zorn2lem3  10263  zorn2lem4  10264  zorn2lem5  10265  zorn2lem7  10267  zornn0g  10270  axdclem2  10285  ondomon  10328  alephval2  10337  cfpwsdom  10349  wuncval2  10512  grupr  10562  gruiun  10564  ingru  10580  grothomex  10594  indpi  10672  nqereu  10694  prlem934  10798  reclem2pr  10813  mulgt0sr  10870  supsrlem  10876  dedekind  11147  lemul1a  11838  squeeze0  11887  peano5nni  11985  nnunb  12238  nn0lt2  12392  nn0le2is012  12393  fzind  12427  nn0ind-raph  12429  zindd  12430  eluzadd  12622  uzin  12627  nn01to3  12690  xnn0xadd0  12990  xmulasslem  13028  icoshft  13214  fzen  13282  uzsubsubfz  13287  elfz0ubfz0  13369  elfz0fzfz0  13370  fz0fzelfz0  13371  elfzmlbp  13376  elfzodifsumelfzo  13462  ssfzo12bi  13491  elfzonelfzo  13498  elfznelfzo  13501  injresinjlem  13516  injresinj  13517  modfzo0difsn  13672  modsumfzodifsn  13673  addmodlteq  13675  ssnn0fi  13714  fsuppmapnn0fiub0  13722  expcllem  13802  expeq0  13822  mulexp  13831  leexp2r  13901  bernneq  13953  facdiv  14010  hasheqf1oi  14075  hashnn0n0nn  14115  hashss  14133  hashgt12el  14146  hashgt12el2  14147  hashimarni  14165  hashle2pr  14200  pr2pwpr  14202  hashge2el2dif  14203  hashge2el2difr  14204  hashtpg  14208  hashge3el3dif  14209  exprelprel  14212  hash1to3  14214  fundmge2nop0  14215  fi1uzind  14220  ccatsymb  14296  swrdnd  14376  swrdnd2  14377  swrdnnn0nd  14378  swrdnd0  14379  pfxnd0  14410  swrdswrdlem  14426  swrdswrd  14427  pfxccatin12lem2a  14449  pfxccatin12lem1  14450  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12lem3  14454  pfxccat3  14456  swrdccat  14457  swrdccat3blem  14461  repsdf2  14500  repswswrd  14506  cshwidxmod  14525  cshwidx0  14528  cshf1  14532  cshweqrep  14543  cshw1  14544  cshwsexa  14546  2cshwcshw  14547  scshwfzeqfzo  14548  cshwcsh2id  14550  wwlktovfo  14682  relexpaddg  14773  iseraltlem2  15403  modfsummods  15514  clim2prod  15609  prodfn0  15615  prodfrec  15616  prodmo  15655  fprodabs  15693  binomfallfac  15760  fprodefsum  15813  dvdsaddre2b  16025  addmodlteqALT  16043  oddge22np1  16067  nn0enne  16095  nn0o1gt2  16099  sumeven  16105  sumodd  16106  dvdslegcd  16220  gcdneg  16238  dfgcd2  16263  rplpwr  16276  lcmf  16347  lcmftp  16350  lcmfunsnlem2lem1  16352  lcmfunsnlem2  16354  lcmfdvdsb  16357  coprmdvds1  16366  qredeq  16371  coprmprod  16375  coprmproddvdslem  16376  cncongr1  16381  cncongr2  16382  prm2orodd  16405  2mulprm  16407  nnnn0modprm0  16516  prm23lt5  16524  prm23ge5  16525  dvdsprmpweqnn  16595  dvdsprmpweqle  16596  oddprmdvds  16613  prmpwdvds  16614  prmreclem4  16629  ramcl  16739  prmgaplem6  16766  prmgaplem7  16767  prmgaplem8  16768  cshwshashlem1  16806  cshwshashlem2  16807  cshwshashlem3  16808  cshwrepswhash1  16813  setsn0fun  16883  setsstruct2  16884  imasleval  17261  mreiincl  17314  mreexexd  17366  inveq  17495  cicsym  17525  cictr  17526  initoid  17725  termoid  17726  initoeu2lem0  17737  initoeu2lem1  17738  initoeu2lem2  17739  initoeu2  17740  fthestrcsetc  17876  fthsetcestrc  17891  drsdirfi  18032  isnmgm  18339  sgrpass  18390  insubm  18466  mgm2nsgrplem3  18568  dfgrp3lem  18682  cyccom  18831  symg2bas  19009  symgfix2  19033  symgextf1  19038  gsmsymgrfix  19045  pmtrprfv3  19071  psgnunilem4  19114  efgi2  19340  0ringnnzr  20549  psgndiflemB  20814  psgndiflemA  20815  elfrlmbasn0  20979  lmictra  21061  mpfrcl  21304  gsummoncoe1  21484  mamufacex  21547  matecl  21583  dmatelnd  21654  dmatscmcl  21661  scmateALT  21670  scmatsgrp1  21680  scmatf1  21689  mavmulsolcl  21709  cramerimplem1  21841  cramerimplem2  21842  pmatcollpw3fi1  21946  mp2pm2mplem4  21967  pm2mpfo  21972  chmaidscmat  22006  fvmptnn04ifb  22009  chfacfscmul0  22016  chfacfpmmul0  22020  cayhamlem1  22024  cayhamlem3  22045  cayleyhamilton1  22050  fiinopn  22059  tgcl  22128  distop  22154  isclo2  22248  iscldtop  22255  ssnei2  22276  opnnei  22280  pnfnei  22380  mnfnei  22381  tgcnp  22413  cnpnei  22424  1stcelcls  22621  txcnpi  22768  cnmptcom  22838  fbfinnfr  23001  isfildlem  23017  snfil  23024  fbunfip  23029  fgcl  23038  elfm2  23108  fmco  23121  fbflim2  23137  cnpflf2  23160  flimfcls  23186  tmdgsum  23255  neibl  23666  tngngpim  23832  fgcfil  24444  caubl  24481  volsuplem  24728  ellimc3  25052  dvnadd  25102  dvnres  25104  cpnord  25108  dvnfre  25125  ply1divex  25310  cxpmul2  25853  zabsle1  26453  gausslemma2dlem1a  26522  gausslemma2dlem3  26525  lgsquad2lem2  26542  2lgs  26564  2sq2  26590  2sqnn0  26595  2sqnn  26596  2sqreultlem  26604  2sqreunnltlem  26607  qabvexp  26783  axcontlem4  27344  umgredgprv  27486  umgrnloop  27487  upgrpredgv  27518  upgredgpr  27521  edglnl  27522  usgredgprvALT  27571  usgrnloopALT  27579  usgredg2v  27603  fusgrfis  27706  nbuhgr2vtx1edgblem  27727  nb3grprlem1  27756  cusgrsize2inds  27829  cusgrfi  27834  fusgrn0degnn0  27875  uspgrloopvtxel  27892  vtxdginducedm1lem4  27918  uhgr0edg0rgrb  27950  wlkl1loop  28014  wlk1walk  28015  upgriswlk  28017  upgrwlkvtxedg  28021  uspgr2wlkeq  28022  wlkv0  28027  wlklenvclwlkOLD  28032  wlksoneq1eq2  28041  wlkon2n0  28043  wlkreslem  28046  wlkres  28047  lfgrwlkprop  28064  pthdivtx  28106  2pthnloop  28108  spthonepeq  28129  uhgrwkspthlem2  28131  uhgrwkspth  28132  usgr2wlkneq  28133  usgr2trlncl  28137  usgr2pthlem  28140  usgr2pth  28141  cyclnspth  28177  lfgrn1cycl  28179  usgr2trlncrct  28180  uspgrn2crct  28182  crctcshwlkn0lem3  28186  crctcshwlkn0lem5  28188  wwlknp  28217  wspthneq1eq2  28234  0enwwlksnge1  28238  wlklnwwlkln1  28242  wlkiswwlks2  28249  wlkiswwlksupgr2  28251  wlklnwwlkln2lem  28256  wwlksnred  28266  wwlksnextbi  28268  wwlksnredwwlkn0  28270  wwlksnextwrd  28271  wwlksnextinj  28273  wwlksnextproplem3  28285  wwlksnextprop  28286  wspthsnwspthsnon  28290  wspthsnonn0vne  28291  2pthon3v  28317  umgr2adedgwlkonALT  28321  umgr2wlk  28323  umgr2wlkon  28324  umgrwwlks2on  28331  elwspths2on  28334  usgr2wspthons3  28338  elwwlks2  28340  rusgrnumwwlk  28349  clwwlkccatlem  28362  clwlkclwwlklem2a4  28370  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  clwlkclwwlkf1lem3  28379  erclwwlkeqlen  28392  clwwlknwwlksn  28411  loopclwwlkn1b  28415  clwwlkf1  28422  wwlksext2clwwlk  28430  eleclclwwlknlem2  28434  umgr2cwwk2dif  28437  eleclclwwlkn  28449  hashecclwwlkn1  28450  umgrhashecclwwlk  28451  clwwlknonwwlknonb  28479  clwwlknonex2lem2  28481  clwwlknonex2  28482  1pthon2v  28526  upgr3v3e3cycl  28553  uhgr3cyclexlem  28554  uhgr3cyclex  28555  eupth2lem3lem4  28604  frgr3vlem1  28646  frgr3vlem2  28647  3vfriswmgrlem  28650  3vfriswmgr  28651  3cyclfrgrrn1  28658  n4cyclfrgr  28664  frgrncvvdeqlem3  28674  frgrncvvdeqlem6  28677  frgrncvvdeqlem7  28678  frgrncvvdeqlem8  28679  frgrwopreglem4a  28683  frgrwopreglem3  28687  frgrwopreg1  28691  frgrwopreg2  28692  frgrwopreglem5lem  28693  frgrwopreglem5ALT  28695  frgrwopreg  28696  fusgr2wsp2nb  28707  2wspmdisj  28710  numclwwlk1lem2foa  28727  numclwwlk1lem2f1  28730  numclwwlk1lem2fo  28731  numclwwlk1  28734  wlkl0  28740  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwlk2lem2f1o  28752  frgrreg  28767  frgrregord013  28768  frgrregord13  28769  friendshipgt3  28771  friendship  28772  eulplig  28856  ipassi  29212  ubthlem2  29242  isch3  29612  shintcli  29700  shmodsi  29760  spansncvi  30023  hoaddsub  30187  eigorthi  30208  pjss2coi  30535  pjnormssi  30539  pj3cor1i  30580  strb  30629  dmdmd  30671  mdsl0  30681  csmdsymi  30705  chrelat2i  30736  mdsymlem3  30776  mdsymlem6  30779  sumdmdlem2  30790  opreu2reuALT  30834  ssrelf  30964  spthcycl  33100  loop1cycl  33108  cvmlift2lem1  33273  satfrel  33338  satfrnmapom  33341  fmlafvel  33356  fmla1  33358  gonarlem  33365  gonar  33366  goalrlem  33367  goalr  33368  satffunlem  33372  satffunlem1lem1  33373  satffunlem2lem1  33375  satffun  33380  satefvfmla1  33396  mrsubvrs  33493  mclsax  33540  3ccased  33672  dfon2lem3  33770  rdgprc  33779  poxp2  33799  frxp2  33800  frxp3  33806  sexp3  33808  naddssim  33846  sltval2  33868  nolt02o  33907  ssltun1  34011  scutun12  34013  madebday  34089  cgrextend  34319  btwndiff  34338  btwnconn1lem12  34409  brsegle  34419  broutsideof2  34433  funray  34451  elicc3  34515  nn0prpwlem  34520  nn0prpw  34521  fnessref  34555  neibastop2lem  34558  filnetlem4  34579  meran1  34609  waj-ax  34612  arg-ax  34614  bj-nnclavc  34737  bj-con2com  34750  bj-axdd2  34783  bj-alrimg  34809  bj-exlimg  34813  bj-exalimi  34823  bj-cbvalimt  34829  bj-eximcom  34833  bj-ssbid1ALT  34855  bj-sb  34878  bj-dtru  35008  bj-snsetex  35162  bj-restpw  35272  bj-finsumval0  35465  mptsnunlem  35518  icoreclin  35537  relowlpssretop  35544  inunissunidif  35555  rdgssun  35558  finorwe  35562  domalom  35584  wl-dral1d  35699  wl-exeq  35702  wl-lem-exsb  35730  poimirlem29  35815  poimirlem32  35818  fdc  35912  seqpo  35914  incsequz  35915  isismty  35968  ismtybndlem  35973  heibor1lem  35976  ismgmOLD  36017  isexid2  36022  ghomco  36058  pridlc  36238  relcnveq3  36463  elrelscnveq3  36616  cdleme18d  38316  tendovalco  38786  cdlemn11pre  39231  dihord2pre  39246  nnadddir  40307  incssnn0  40540  fphpd  40645  jm2.19lem3  40820  setindtr  40853  islssfg2  40903  mpaaeu  40982  pr2cv  41162  refimssco  41222  iunrelexpmin1  41323  iunrelexpmin2  41327  trclimalb2  41341  clsk1indlem3  41660  tfindsd  41830  mnurndlem1  41906  nzss  41942  sb5ALT  42152  truniALT  42168  ee223  42261  3orbi123VD  42477  sbc3orgVD  42478  exbirVD  42480  exbiriVD  42481  sbcim2gVD  42502  trsbcVD  42504  truniALTVD  42505  onfrALTlem3VD  42514  onfrALTlem2VD  42516  csbrngVD  42523  19.41rgVD  42529  ax6e2eqVD  42534  ax6e2ndeqVD  42536  2uasbanhVD  42538  sb5ALTVD  42540  vk15.4jVD  42541  infxrunb3rnmpt  42975  stoweidlem26  43574  hirstL-ax3  44398  rexsb  44602  rexrsb  44603  euoreqb  44612  2reu8i  44616  afvres  44675  tz6.12-afv  44676  afvco2  44679  afv2orxorb  44731  afv2res  44742  tz6.12-afv2  44743  tz6.12i-afv2  44746  dfatcolem  44758  zm1nn  44805  fzoopth  44830  2ffzoeq  44831  smonoord  44834  iccpartiltu  44885  iccpartlt  44887  iccpartltu  44888  iccpartgtl  44889  iccpartgt  44890  iccpartleu  44891  iccpartgel  44892  icceuelpart  44899  iccpartnel  44901  lswn0  44907  ichnreuop  44935  ichreuopeq  44936  prsprel  44950  sprsymrelfvlem  44953  sprsymrelf1lem  44954  sprsymrelfolem2  44956  prproropf1olem4  44969  paireqne  44974  prprelb  44979  reupr  44985  goldbachth  45010  odz2prm2pw  45026  fmtno4prmfac  45035  fmtno4prmfac193  45036  prmdvdsfmtnof1lem2  45048  2pwp1prmfmtno  45053  lighneallem2  45069  lighneallem4b  45072  lighneallem4  45073  requad2  45086  odd2prm2  45181  mogoldbblem  45183  gbepos  45221  gbowgt5  45225  gbowge7  45226  stgoldbwt  45239  sbgoldbwt  45240  sbgoldbst  45241  sbgoldbaltlem1  45242  sbgoldbalt  45244  sbgoldbo  45250  nnsum3primesle9  45257  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  bgoldbtbndlem1  45268  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbnd  45272  isomuspgrlem1  45290  upgrwlkupwlk  45313  uspgrsprf1  45320  mgmhmlin  45351  issubmgm2  45355  lmod0rng  45437  lidldomn1  45490  lidlmmgm  45494  rnghmsscmap  45543  rnghmsubcsetclem2  45545  rngcinv  45550  rngccatidALTV  45558  rngcinvALTV  45562  funcrngcsetc  45567  funcrngcsetcALT  45568  rhmsscmap  45589  rhmsubcsetclem2  45591  rhmsubcrngclem2  45597  ringcinv  45601  ringcbasbas  45603  funcringcsetc  45604  funcringcsetcALTV2lem9  45613  ringccatidALTV  45621  ringcinvALTV  45625  ringcbasbasALTV  45627  rhmsubclem4  45658  rhmsubcALTVlem4  45676  ztprmneprm  45694  pgrpgt2nabl  45713  lmodvsmdi  45729  ply1mulgsumlem2  45739  lincsumcl  45783  ellcoellss  45787  linindslinci  45800  islinindfis  45801  lincext3  45808  lindslinindimp2lem4  45813  lindslinindsimp2lem5  45814  lindslinindsimp2  45815  lindsrng01  45820  ldepspr  45825  lincresunit3lem1  45831  elfzolborelfzop1  45871  dignn0ldlem  45959  nn0sumshdiglem1  45978  1arymaptf1  45999  2arymaptf1  46010  rrx2xpref1o  46075  rrx2plord2  46079  rrx2plordisom  46080  line2ylem  46108  line2xlem  46110  line2y  46112  itschlc0xyqsol1  46123  inlinecirc02plem  46143  fullthinc  46338  tfis2d  46397  onsetrec  46424