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  5415  iunopeqop  5429  fveqdmss  6938  f1o2ndf1  7934  wfrlem12OLD  8122  fiint  9021  dfac5  9815  ltexprlem7  10729  rpnnen1lem5  12650  fz0fzdiffz0  13294  elfzodifsumelfzo  13381  ssfzo12  13408  elfznelfzo  13420  injresinjlem  13435  addmodlteq  13594  suppssfz  13642  fi1uzind  14139  swrdswrd  14346  cshf1  14451  s3iunsndisj  14607  dfgcd2  16182  cncongr1  16300  infpnlem1  16539  prmgaplem6  16685  initoeu1  17642  termoeu1  17649  cply1mul  21375  pm2mpf1  21856  mp2pm2mplem4  21866  neindisj2  22182  alexsubALTlem3  23108  2sqreultlem  26500  2sqreunnltlem  26503  nbuhgr2vtx1edgblem  27621  cusgrsize2inds  27723  2pthnloop  28000  upgrwlkdvdelem  28005  usgr2pthlem  28032  wwlksnextbi  28160  wspn0  28190  rusgrnumwwlks  28240  clwlkclwwlklem2a  28263  clwlkclwwlklem2  28265  clwwlkf  28312  clwwlknonex2lem2  28373  uhgr3cyclexlem  28446  3cyclfrgrrn1  28550  frgrnbnb  28558  frgrncvvdeqlem9  28572  frgrwopreglem2  28578  frgrregord013  28660  friendship  28664  spansncvi  29915  cdj3lem2b  30700  sat1el2xp  33241  bj-cbvalim  34753  bj-cbvexim  34754  zerdivemp1x  36032  ee233  42028  funbrafv  44537  ssfz12  44694  iccpartnel  44778  poprelb  44864  lighneal  44951  tgoldbach  45157  isomuspgrlem2d  45171  lidldomn1  45367  rngccatidALTV  45435  ringccatidALTV  45498  ply1mulgsumlem1  45615  lindslinindsimp2  45692  nn0sumshdiglemA  45853  nn0sumshdiglemB  45854