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  5100  iunopeqop  5114  predpo  5841  fveqdmss  6497  f1o2ndf1  7436  wfrlem12  7579  fiint  8393  dfac5  9151  ltexprlem7  10066  rpnnen1lem5  12021  rpnnen1lem5OLD  12027  difreicc  12511  fz0fzdiffz0  12656  elfzodifsumelfzo  12742  ssfzo12  12769  elfznelfzo  12781  injresinjlem  12796  addmodlteq  12953  suppssfz  13001  fi1uzind  13481  swrdswrd  13669  cshf1  13765  s3iunsndisj  13917  dfgcd2  15471  cncongr1  15588  infpnlem1  15821  prmgaplem6  15967  initoeu1  16868  termoeu1  16875  cply1mul  19879  pm2mpf1  20824  mp2pm2mplem4  20834  neindisj2  21148  alexsubALTlem3  22073  nbuhgr2vtx1edgblem  26470  cusgrsize2inds  26584  2pthnloop  26862  upgrwlkdvdelem  26867  usgr2pthlem  26894  wwlksnextbi  27038  wspn0  27071  rusgrnumwwlks  27123  clwlkclwwlklem2a  27148  clwlkclwwlklem2  27150  clwwlkf  27203  clwlksfclwwlkOLD  27243  clwwlknonwwlknonb  27281  clwwlknonex2lem2  27284  uhgr3cyclexlem  27361  3cyclfrgrrn1  27467  frgrnbnb  27475  frgrncvvdeqlem9  27489  frgrwopreglem2  27495  frgrregord013  27594  friendship  27598  spansncvi  28851  cdj3lem2b  29636  zerdivemp1x  34078  ee233  39250  funbrafv  41758  ssfz12  41852  iccpartnel  41902  lighneal  42056  tgoldbach  42233  tgoldbachOLD  42240  lidldomn1  42449  rngccatidALTV  42517  ringccatidALTV  42580  ply1mulgsumlem1  42702  lindslinindsimp2  42780  nn0sumshdiglemA  42941  nn0sumshdiglemB  42942
  Copyright terms: Public domain W3C validator