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  5455  iunopeqop  5469  iunopeqopOLD  5470  fveqdmss  7026  f1o2ndf1  8068  fiint  9234  dfac5  10049  ltexprlem7  10963  rpnnen1lem5  12929  fz0fzdiffz0  13589  elfzodifsumelfzo  13684  ssfzo12  13712  elfznelfzo  13726  injresinjlem  13743  addmodlteq  13906  suppssfz  13954  fi1uzind  14467  swrdswrd  14665  cshf1  14770  s3iunsndisj  14928  dfgcd2  16513  cncongr1  16634  infpnlem1  16879  prmgaplem6  17025  initoeu1  17976  termoeu1  17983  cply1mul  22289  pm2mpf1  22789  mp2pm2mplem4  22799  neindisj2  23113  alexsubALTlem3  24039  2sqreultlem  27435  2sqreunnltlem  27438  nbuhgr2vtx1edgblem  29445  cusgrsize2inds  29547  2pthnloop  29824  upgrwlkdvdelem  29829  usgr2pthlem  29856  cyclnumvtx  29893  wwlksnextbi  29987  wspn0  30017  rusgrnumwwlks  30070  clwlkclwwlklem2a  30093  clwlkclwwlklem2  30095  clwwlkf  30142  clwwlknonex2lem2  30203  uhgr3cyclexlem  30276  3cyclfrgrrn1  30380  frgrnbnb  30388  frgrncvvdeqlem9  30402  frgrwopreglem2  30408  frgrregord013  30490  friendship  30494  spansncvi  31748  cdj3lem2b  32533  sat1el2xp  35614  zerdivemp1x  38321  ee233  44970  funbrafv  47628  ssfz12  47784  nnmul2b  47801  iccpartnel  47920  poprelb  48006  lighneal  48096  tgoldbach  48315  clnbgrgrim  48432  lidldomn1  48729  rngccatidALTV  48770  ringccatidALTV  48804  ply1mulgsumlem1  48884  lindslinindsimp2  48961  nn0sumshdiglemA  49117  nn0sumshdiglemB  49118