Theorem com14 97

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 93	. 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏))))
3	2	com3r 88	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  5492  iunopeqop  5506  iunopeqopOLD  5507  fveqdmss  7075  f1o2ndf1  8118  fiint  9287  dfac5  10113  ltexprlem7  11028  rpnnen1lem5  13006  fz0fzdiffz0  13667  elfzodifsumelfzo  13762  ssfzo12  13790  elfznelfzo  13804  injresinjlem  13821  addmodlteq  13984  suppssfz  14032  fi1uzind  14546  swrdswrd  14744  cshf1  14849  s3iunsndisj  15007  dfgcd2  16605  cncongr1  16726  infpnlem1  16971  prmgaplem6  17117  initoeu1  18069  termoeu1  18076  cply1mul  22437  pm2mpf1  22937  mp2pm2mplem4  22947  neindisj2  23261  alexsubALTlem3  24187  2sqreultlem  27592  2sqreunnltlem  27595  nbuhgr2vtx1edgblem  29682  cusgrsize2inds  29784  2pthnloop  30061  upgrwlkdvdelem  30066  usgr2pthlem  30093  cyclnumvtx  30130  wwlksnextbi  30224  wspn0  30254  rusgrnumwwlks  30307  clwlkclwwlklem2a  30330  clwlkclwwlklem2  30332  clwwlkf  30379  clwwlknonex2lem2  30440  uhgr3cyclexlem  30513  3cyclfrgrrn1  30617  frgrnbnb  30625  frgrncvvdeqlem9  30639  frgrwopreglem2  30645  frgrregord013  30727  friendship  30731  spansncvi  31985  cdj3lem2b  32770  sat1el2xp  35852  zerdivemp1x  38579  ee233  45211  funbrafv  47878  ssfz12  48034  nnmul2b  48051  iccpartnel  48170  poprelb  48256  lighneal  48346  tgoldbach  48565  clnbgrgrim  48682  lidldomn1  48979  rngccatidALTV  49020  ringccatidALTV  49054  ply1mulgsumlem1  49149  lindslinindsimp2  49226  nn0sumshdiglemA  49382  nn0sumshdiglemB  49383