Theorem com24 95

Description: Commutation of antecedents. Swap 2nd and 4th. Deduction associated with com13 88. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.)

Hypothesis

Ref	Expression
com4.1	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))

Assertion

Ref	Expression
com24	⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → 𝜏))))

Proof of Theorem com24

Step	Hyp	Ref	Expression
1		com4.1	. . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏))))
2	1	com4t 93	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com13 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:  com25  99  propeqop  5503  po2ne  5600  fveqdmss  7082  tfrlem9  8399  omordi  8580  nnmordi  8645  fundmen  9049  pssnn  9186  pssnnOLD  9283  fiint  9342  infssuni  9361  cfcoflem  10289  fin1a2lem10  10426  axdc3lem2  10468  zorn2lem7  10519  fpwwe2lem11  10658  genpnnp  11022  mulgt0sr  11122  nn01to3  12949  elfzodifsumelfzo  13724  ssfzo12  13751  elfznelfzo  13763  injresinjlem  13778  injresinj  13779  ssnn0fi  13976  expcan  14159  ltexp2  14160  hashgt12el2  14408  fi1uzind  14484  swrdswrdlem  14680  swrdswrd  14681  wrd2ind  14699  swrdccatin1  14701  cshwlen  14775  2cshwcshw  14802  cshwcsh2id  14805  dvdsmodexp  16232  dvdsaddre2b  16277  lcmfunsnlem2lem1  16602  lcmfdvdsb  16607  coprmproddvdslem  16626  infpnlem1  16872  cshwshashlem1  17058  initoeu1  17993  initoeu2lem1  17996  initoeu2  17998  termoeu1  18000  grpinveu  18924  mulgass2  20238  lss1d  20840  nzerooringczr  21399  cply1mul  22208  gsummoncoe1  22220  mp2pm2mplem4  22704  chpscmat  22737  chcoeffeq  22781  cnpnei  23161  hausnei2  23250  cmpsublem  23296  comppfsc  23429  filufint  23817  flimopn  23872  flimrest  23880  alexsubALTlem3  23946  equivcfil  25220  dvfsumrlim3  25961  pntlem3  27535  elntg2  28789  numedglnl  28950  cusgrsize2inds  29260  2pthnloop  29538  usgr2wlkneq  29563  elwspths2on  29764  clwwlkccatlem  29792  clwlkclwwlklem2a  29801  clwwisshclwws  29818  erclwwlktr  29825  erclwwlkntr  29874  3cyclfrgrrn1  30088  vdgn1frgrv2  30099  frgrncvvdeqlem8  30109  frgrwopreglem5  30124  frgrwopreglem5ALT  30125  frgr2wwlkeqm  30134  2clwwlk2clwwlk  30153  frgrregord013  30198  grpoinveu  30322  elspansn4  31376  atomli  32185  mdsymlem3  32208  mdsymlem5  32210  sat1el2xp  34983  satffunlem  35005  satffunlem1lem1  35006  satffunlem2lem1  35008  nn0prpwlem  35800  axc11n11r  36154  broucube  37121  rngoueqz  37407  rngonegrmul  37411  zerdivemp1x  37414  lshpdisj  38453  linepsubN  39219  pmapsub  39235  paddasslem5  39291  dalaw  39353  pclclN  39358  pclfinN  39367  trlval2  39630  tendospcanN  40490  diaintclN  40525  dibintclN  40634  dihintcl  40811  dvh4dimlem  40910  com3rgbi  43947  2reu8i  46487  ssfz12  46688  iccpartlt  46758  iccelpart  46767  iccpartnel  46772  fargshiftf1  46775  fargshiftfva  46777  sbcpr  46855  reuopreuprim  46860  lighneallem3  46941  lighneal  46945  sbgoldbwt  47111  isuspgrimlem  47166  grimcnv  47171  grimco  47172  lindslinindsimp1  47519