MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com13 Structured version   Visualization version   GIF version

Theorem com13 85
Description: Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com3.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
com13 (𝜒 → (𝜓 → (𝜑𝜃)))

Proof of Theorem com13
StepHypRef Expression
1 com3.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21com3r 84 . 2 (𝜒 → (𝜑 → (𝜓𝜃)))
32com23 83 1 (𝜒 → (𝜓 → (𝜑𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  com24  92  imim12  102  an13s  840  an31s  843  3imp31  1249  meredith  1556  predpo  5601  funopg  5822  eldmrexrnb  6259  fvn0fvelrn  6313  peano5  6959  f1o2ndf1  7150  suppimacnv  7171  omordi  7511  omeulem1  7527  brecop  7705  isinf  8036  fiint  8100  carduni  8668  dfac5  8812  dfac2  8814  cofsmo  8952  cfcoflem  8955  domtriomlem  9125  axdc3lem2  9134  nqereu  9608  squeeze0  10778  zmax  11620  xrsupsslem  11968  xrinfmsslem  11969  supxrunb1  11980  supxrunb2  11981  difreicc  12134  elfz0ubfz0  12270  elfz0fzfz0  12271  fz0fzelfz0  12272  fz0fzdiffz0  12275  fzo1fzo0n0  12344  elfzodifsumelfzo  12359  ssfzo12  12385  ssfzo12bi  12387  elfznelfzo  12397  injresinjlem  12408  injresinj  12409  addmodlteq  12565  uzindi  12601  ssnn0fi  12604  suppssfz  12614  facwordi  12896  hasheqf1oi  12957  hasheqf1oiOLD  12958  hashf1rn  12959  hashf1rnOLD  12960  hash2prde  13064  swrdswrdlem  13260  swrdswrd  13261  wrd2ind  13278  reuccats1lem  13280  swrdccatin1  13283  swrdccatin12lem2  13289  swrdccat  13293  repsdf2  13325  cshwidx0  13352  cshweqrep  13367  2cshwcshw  13371  cshwcsh2id  13374  swrdco  13383  wwlktovfo  13498  sqrt2irr  14766  oddnn02np1  14859  oddge22np1  14860  evennn02n  14861  evennn2n  14862  dfgcd2  15050  lcmf  15133  lcmfunsnlem2lem2  15139  initoeu2lem1  16436  symgfix2  17608  gsmsymgreqlem2  17623  psgnunilem4  17689  lmodfopnelem1  18671  01eq0ring  19042  cply1mul  19434  gsummoncoe1  19444  mamufacex  19962  matecl  19998  gsummatr01lem4  20231  gsummatr01  20232  mp2pm2mplem4  20381  chfacfscmul0  20430  chfacfpmmul0  20434  cayhamlem1  20438  fbunfip  21431  tngngp3  22218  zabsle1  24766  gausslemma2dlem1a  24835  2lgsoddprm  24886  usgranloopv  25701  usgraedg4  25710  usgraidx2vlem2  25715  usgrafisbase  25737  nbgra0nb  25752  nbgraf1olem3  25766  nbgraf1olem5  25768  nbcusgra  25786  cusgrasize2inds  25799  cusgrafi  25804  usgrasscusgra  25805  sizeusglecusglem1  25806  sizeusglecusg  25808  uvtxnbgra  25815  spthonepeq  25911  1pthoncl  25916  wlkdvspthlem  25931  usgra2adedgspthlem2  25934  usgra2wlkspthlem1  25941  usgra2wlkspth  25943  cyclnspth  25953  fargshiftf1  25959  usgrcyclnl2  25963  nvnencycllem  25965  3v3e3cycl1  25966  4cycl4v4e  25988  4cycl4dv4e  25990  usg2wlkeq  26030  wwlknextbi  26047  wwlknredwwlkn0  26049  wwlkextinj  26052  clwwlkgt0  26093  clwlkisclwwlklem2a1  26101  clwlkisclwwlklem2fv2  26105  clwlkisclwwlklem2a4  26106  clwlkisclwwlklem2a  26107  clwlkisclwwlklem1  26109  clwwlkext2edg  26124  clwwisshclww  26129  erclwwlktr  26137  usg2cwwk2dif  26142  erclwwlkntr  26149  clwlkf1clwwlklem  26170  el2wlkonotot0  26193  usg2wlkonot  26204  usg2wotspth  26205  usgfidegfi  26231  hashnbgravdg  26234  frgraunss  26316  frgra3vlem1  26321  3cyclfrgrarn1  26333  3cyclfrgrarn  26334  4cycl2vnunb  26338  frgranbnb  26341  vdn0frgrav2  26344  vdn1frgrav2  26346  usgn0fidegnn0  26350  frgrancvvdeqlemB  26359  frgrawopreglem2  26366  frg2wot1  26378  usg2spot2nb  26386  2spotmdisj  26389  clwwlkextfrlem1  26397  extwwlkfablem2  26399  numclwlk1lem2fo  26416  frgrareggt1  26437  frgrareg  26438  friendshipgt3  26442  shmodsi  27466  kbass6  28198  mdsymlem6  28485  mdsymlem7  28486  cdj3lem2a  28513  cdj3lem3a  28516  wl-spae  32309  grpomndo  32668  rngoueqz  32733  zerdivemp1x  32740  elpcliN  34021  relexpiidm  36839  relexpxpmin  36852  ntrk0kbimka  37181  eel12131  37783  tratrbVD  37943  2uasbanhVD  37993  funressnfv  39681  funbrafv  39712  iccpartgt  39790  iccelpart  39796  iccpartnel  39801  fmtno4prmfac  39847  lighneallem4b  39889  lighneal  39891  gbegt5  40008  sgoldbaltlem1  40026  bgoldbtbndlem2  40047  bgoldbtbndlem3  40048  bgoldbtbndlem4  40049  bgoldbtbnd  40050  pfxccatin12lem2  40112  reuccatpfxs1lem  40121  reuccatpfxs1  40122  propeqop  40146  otiunsndisjX  40152  fundmge2nop0  40172  ssfz12  40198  fzoopth  40207  umgrnloopv  40353  upgredg2vtx  40395  usgruspgrb  40433  usgrnloopvALT  40450  usgredg2vlem2  40475  edg0usgr  40501  nbuhgr  40587  nbumgr  40591  nbuhgr2vtx1edgblem  40595  cusgredg  40668  cusgrsize2inds  40691  sizusglecusg  40701  umgr2v2enb1  40764  rusgr1vtx  40810  upgrewlkle2  40830  uspgr2wlkeq  40876  1wlkreslem  40900  spthonepeq-av  40980  usgr2wlkneq  40984  usgr2trlspth  40989  usgr2pth  40992  clwlkl1loop  41011  lfgrn1cycl  41030  uspgrn2crct  41033  crctcsh1wlkn0lem3  41037  crctcsh1wlkn0lem5  41039  wwlksnextbi  41122  wwlksnredwwlkn0  41124  wwlksnextinj  41127  wspthsnonn0vne  41146  umgr2adedgspth  41177  umgr2wlk  41178  usgr2wspthons3  41189  clwlkclwwlklem2a1  41223  clwlkclwwlklem2fv2  41227  clwlkclwwlklem2a4  41228  clwlkclwwlklem2a  41229  clwlkclwwlklem2  41231  clwwlksext2edg  41252  clwwisshclwws  41257  erclwwlkstr  41265  erclwwlksntr  41277  upgr11wlkdlem1  41334  upgr3v3e3cycl  41369  uhgr3cyclex  41371  upgr4cycl4dv4e  41374  eucrctshift  41433  frgr3vlem1  41465  3cyclfrgrrn1  41477  3cyclfrgrrn  41478  4cycl2vnunb-av  41482  frgrnbnb  41485  frgrncvvdeqlemB  41499  frgr2wwlk1  41516  av-numclwwlkffin0  41535  av-numclwlk1lem2fo  41547  av-frgrareg  41570  av-friendshipgt3  41574  lidldomn1  41733  2zrngamgm  41751  rngccatidALTV  41803  ringccatidALTV  41866  nzerooringczr  41886  scmsuppss  41969  ply1mulgsumlem1  41990  lincsumcl  42036  ellcoellss  42040  lindslinindsimp1  42062  lindslinindimp2lem1  42063  nn0sumshdiglemA  42233  nn0sumshdiglemB  42234
  Copyright terms: Public domain W3C validator