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  5388  iunopeqop  5402  predpo  6159  fveqdmss  6838  f1o2ndf1  7807  wfrlem12  7955  fiint  8783  dfac5  9542  ltexprlem7  10452  rpnnen1lem5  12368  fz0fzdiffz0  13004  elfzodifsumelfzo  13091  ssfzo12  13118  elfznelfzo  13130  injresinjlem  13145  addmodlteq  13302  suppssfz  13350  fi1uzind  13843  swrdswrd  14055  cshf1  14160  s3iunsndisj  14316  dfgcd2  15882  cncongr1  15999  infpnlem1  16234  prmgaplem6  16380  initoeu1  17259  termoeu1  17266  cply1mul  20390  pm2mpf1  21335  mp2pm2mplem4  21345  neindisj2  21659  alexsubALTlem3  22585  2sqreultlem  25950  2sqreunnltlem  25953  nbuhgr2vtx1edgblem  27060  cusgrsize2inds  27162  2pthnloop  27439  upgrwlkdvdelem  27444  usgr2pthlem  27471  wwlksnextbi  27599  wspn0  27630  rusgrnumwwlks  27680  clwlkclwwlklem2a  27703  clwlkclwwlklem2  27705  clwwlkf  27753  clwwlknonex2lem2  27814  uhgr3cyclexlem  27887  3cyclfrgrrn1  27991  frgrnbnb  27999  frgrncvvdeqlem9  28013  frgrwopreglem2  28019  frgrregord013  28101  friendship  28105  spansncvi  29356  cdj3lem2b  30141  sat1el2xp  32523  bj-cbvalim  33875  bj-cbvexim  33876  zerdivemp1x  35106  ee233  40730  funbrafv  43234  ssfz12  43391  iccpartnel  43475  poprelb  43563  lighneal  43653  tgoldbach  43859  isomuspgrlem2d  43873  lidldomn1  44120  rngccatidALTV  44188  ringccatidALTV  44251  ply1mulgsumlem1  44368  lindslinindsimp2  44446  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608
  Copyright terms: Public domain W3C validator