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

Step	Hyp	Ref	Expression
1		com4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4l 92	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com3r 87	1 ⊢ (𝜃 → (𝜓 → (𝜒 → (𝜑 → 𝜏))))

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  5447  iunopeqop  5461  fveqdmss  7011  f1o2ndf1  8052  fiint  9211  dfac5  10020  ltexprlem7  10933  rpnnen1lem5  12879  fz0fzdiffz0  13537  elfzodifsumelfzo  13631  ssfzo12  13659  elfznelfzo  13673  injresinjlem  13690  addmodlteq  13853  suppssfz  13901  fi1uzind  14414  swrdswrd  14612  cshf1  14717  s3iunsndisj  14875  dfgcd2  16457  cncongr1  16578  infpnlem1  16822  prmgaplem6  16968  initoeu1  17918  termoeu1  17925  cply1mul  22212  pm2mpf1  22715  mp2pm2mplem4  22725  neindisj2  23039  alexsubALTlem3  23965  2sqreultlem  27386  2sqreunnltlem  27389  nbuhgr2vtx1edgblem  29330  cusgrsize2inds  29433  2pthnloop  29710  upgrwlkdvdelem  29715  usgr2pthlem  29742  cyclnumvtx  29779  wwlksnextbi  29873  wspn0  29903  rusgrnumwwlks  29953  clwlkclwwlklem2a  29976  clwlkclwwlklem2  29978  clwwlkf  30025  clwwlknonex2lem2  30086  uhgr3cyclexlem  30159  3cyclfrgrrn1  30263  frgrnbnb  30271  frgrncvvdeqlem9  30285  frgrwopreglem2  30291  frgrregord013  30373  friendship  30377  spansncvi  31630  cdj3lem2b  32415  sat1el2xp  35421  bj-cbvalim  36685  bj-cbvexim  36686  zerdivemp1x  37993  ee233  44558  funbrafv  47195  ssfz12  47351  iccpartnel  47475  poprelb  47561  lighneal  47648  tgoldbach  47854  clnbgrgrim  47971  lidldomn1  48268  rngccatidALTV  48309  ringccatidALTV  48343  ply1mulgsumlem1  48424  lindslinindsimp2  48501  nn0sumshdiglemA  48657  nn0sumshdiglemB  48658