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

Theorem com14 96
Description: Commutation of antecedents. Swap 1st and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)
Hypothesis
Ref Expression
com4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
com14 (𝜃 → (𝜓 → (𝜒 → (𝜑𝜏))))

Proof of Theorem com14
StepHypRef Expression
1 com4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21com4l 92 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
32com3r 87 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:  propeqop  4930  iunopeqop  4941  predpo  5657  fveqdmss  6310  f1o2ndf1  7230  wfrlem12  7371  fiint  8181  dfac5  8895  ltexprlem7  9808  rpnnen1lem5  11762  rpnnen1lem5OLD  11768  difreicc  12246  fz0fzdiffz0  12389  elfzodifsumelfzo  12474  ssfzo12  12502  elfznelfzo  12514  injresinjlem  12528  addmodlteq  12685  suppssfz  12734  fi1uzind  13218  fi1uzindOLD  13224  swrdswrd  13398  cshf1  13493  s3iunsndisj  13641  dfgcd2  15187  cncongr1  15305  infpnlem1  15538  prmgaplem6  15684  initoeu1  16582  termoeu1  16589  cply1mul  19583  pm2mpf1  20523  mp2pm2mplem4  20533  neindisj2  20837  alexsubALTlem3  21763  nbuhgr2vtx1edgblem  26134  cusgrsize2inds  26236  2pthnloop  26496  upgrwlkdvdelem  26501  usgr2pthlem  26528  wwlksnextbi  26658  rusgrnumwwlks  26736  clwlkclwwlklem2a  26766  clwlkclwwlklem2  26768  clwwlksf  26781  clwlksfclwwlk  26828  uhgr3cyclexlem  26907  3cyclfrgrrn1  27013  frgrnbnb  27021  frgrncvvdeqlemC  27036  numclwlk1lem2foa  27079  frgrregord013  27107  friendship  27111  spansncvi  28357  cdj3lem2b  29142  frrlem11  31490  zerdivemp1x  33375  ee233  38204  funbrafv  40539  ssfz12  40618  iccpartnel  40669  lighneal  40824  tgoldbach  40990  tgoldbachOLD  40997  lidldomn1  41206  rngccatidALTV  41274  ringccatidALTV  41337  ply1mulgsumlem1  41459  lindslinindsimp2  41537  nn0sumshdiglemA  41702  nn0sumshdiglemB  41703
  Copyright terms: Public domain W3C validator