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  5422  iunopeqop  5436  fveqdmss  6965  f1o2ndf1  7972  wfrlem12OLD  8160  fiint  9100  dfac5  9893  ltexprlem7  10807  rpnnen1lem5  12730  fz0fzdiffz0  13374  elfzodifsumelfzo  13462  ssfzo12  13489  elfznelfzo  13501  injresinjlem  13516  addmodlteq  13675  suppssfz  13723  fi1uzind  14220  swrdswrd  14427  cshf1  14532  s3iunsndisj  14688  dfgcd2  16263  cncongr1  16381  infpnlem1  16620  prmgaplem6  16766  initoeu1  17735  termoeu1  17742  cply1mul  21474  pm2mpf1  21957  mp2pm2mplem4  21967  neindisj2  22283  alexsubALTlem3  23209  2sqreultlem  26604  2sqreunnltlem  26607  nbuhgr2vtx1edgblem  27727  cusgrsize2inds  27829  2pthnloop  28108  upgrwlkdvdelem  28113  usgr2pthlem  28140  wwlksnextbi  28268  wspn0  28298  rusgrnumwwlks  28348  clwlkclwwlklem2a  28371  clwlkclwwlklem2  28373  clwwlkf  28420  clwwlknonex2lem2  28481  uhgr3cyclexlem  28554  3cyclfrgrrn1  28658  frgrnbnb  28666  frgrncvvdeqlem9  28680  frgrwopreglem2  28686  frgrregord013  28768  friendship  28772  spansncvi  30023  cdj3lem2b  30808  sat1el2xp  33350  bj-cbvalim  34835  bj-cbvexim  34836  zerdivemp1x  36114  ee233  42146  funbrafv  44661  ssfz12  44817  iccpartnel  44901  poprelb  44987  lighneal  45074  tgoldbach  45280  isomuspgrlem2d  45294  lidldomn1  45490  rngccatidALTV  45558  ringccatidALTV  45621  ply1mulgsumlem1  45738  lindslinindsimp2  45815  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977