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  4999  iunopeqop  5010  predpo  5736  fveqdmss  6394  f1o2ndf1  7330  wfrlem12  7471  fiint  8278  dfac5  8989  ltexprlem7  9902  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  difreicc  12342  fz0fzdiffz0  12487  elfzodifsumelfzo  12573  ssfzo12  12601  elfznelfzo  12613  injresinjlem  12628  addmodlteq  12785  suppssfz  12834  fi1uzind  13317  swrdswrd  13506  cshf1  13602  s3iunsndisj  13753  dfgcd2  15310  cncongr1  15428  infpnlem1  15661  prmgaplem6  15807  initoeu1  16708  termoeu1  16715  cply1mul  19712  pm2mpf1  20652  mp2pm2mplem4  20662  neindisj2  20975  alexsubALTlem3  21900  nbuhgr2vtx1edgblem  26292  cusgrsize2inds  26405  2pthnloop  26683  upgrwlkdvdelem  26688  usgr2pthlem  26715  wwlksnextbi  26857  wspn0  26889  rusgrnumwwlks  26941  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwwlkf  27010  clwlksfclwwlk  27049  clwwlknonwwlknonb  27080  clwwlknonex2lem2  27083  uhgr3cyclexlem  27159  3cyclfrgrrn1  27265  frgrnbnb  27273  frgrncvvdeqlem9  27287  frgrwopreglem2  27293  frgrregord013  27382  friendship  27386  spansncvi  28639  cdj3lem2b  29424  zerdivemp1x  33876  ee233  39042  funbrafv  41559  ssfz12  41649  iccpartnel  41699  lighneal  41853  tgoldbach  42030  tgoldbachOLD  42037  lidldomn1  42246  rngccatidALTV  42314  ringccatidALTV  42377  ply1mulgsumlem1  42499  lindslinindsimp2  42577  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator