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  5475  iunopeqop  5489  iunopeqopOLD  5490  fveqdmss  7055  f1o2ndf1  8096  fiint  9267  dfac5  10082  ltexprlem7  10997  rpnnen1lem5  12979  fz0fzdiffz0  13639  elfzodifsumelfzo  13734  ssfzo12  13762  elfznelfzo  13776  injresinjlem  13793  addmodlteq  13956  suppssfz  14004  fi1uzind  14517  swrdswrd  14715  cshf1  14820  s3iunsndisj  14978  dfgcd2  16563  cncongr1  16684  infpnlem1  16929  prmgaplem6  17075  initoeu1  18027  termoeu1  18034  cply1mul  22339  pm2mpf1  22839  mp2pm2mplem4  22849  neindisj2  23163  alexsubALTlem3  24089  2sqreultlem  27488  2sqreunnltlem  27491  nbuhgr2vtx1edgblem  29498  cusgrsize2inds  29600  2pthnloop  29877  upgrwlkdvdelem  29882  usgr2pthlem  29909  cyclnumvtx  29946  wwlksnextbi  30040  wspn0  30070  rusgrnumwwlks  30123  clwlkclwwlklem2a  30146  clwlkclwwlklem2  30148  clwwlkf  30195  clwwlknonex2lem2  30256  uhgr3cyclexlem  30329  3cyclfrgrrn1  30433  frgrnbnb  30441  frgrncvvdeqlem9  30455  frgrwopreglem2  30461  frgrregord013  30543  friendship  30547  spansncvi  31801  cdj3lem2b  32586  sat1el2xp  35693  zerdivemp1x  38410  ee233  45059  funbrafv  47716  ssfz12  47872  nnmul2b  47889  iccpartnel  48008  poprelb  48094  lighneal  48184  tgoldbach  48403  clnbgrgrim  48520  lidldomn1  48817  rngccatidALTV  48858  ringccatidALTV  48892  ply1mulgsumlem1  48972  lindslinindsimp2  49049  nn0sumshdiglemA  49205  nn0sumshdiglemB  49206