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  5454  po2ne  5547  fveqdmss  7016  resf1extb  7874  tfrlem9  8314  omordi  8491  nnmordi  8556  fundmen  8963  pssnn  9092  fiint  9235  fiintOLD  9236  infssuni  9255  cfcoflem  10185  fin1a2lem10  10322  axdc3lem2  10364  zorn2lem7  10415  fpwwe2lem11  10554  genpnnp  10918  mulgt0sr  11018  nn01to3  12860  fzdif1  13526  elfzodifsumelfzo  13652  ssfzo12  13680  elfznelfzo  13693  injresinjlem  13708  injresinj  13709  ssnn0fi  13910  expcan  14094  ltexp2  14095  hashgt12el2  14348  fi1uzind  14432  swrdswrdlem  14628  swrdswrd  14629  wrd2ind  14647  swrdccatin1  14649  cshwlen  14723  2cshwcshw  14750  cshwcsh2id  14753  dvdsmodexp  16189  dvdsaddre2b  16236  lcmfunsnlem2lem1  16567  lcmfdvdsb  16572  coprmproddvdslem  16591  infpnlem1  16840  cshwshashlem1  17025  initoeu1  17936  initoeu2lem1  17939  initoeu2  17941  termoeu1  17943  grpinveu  18871  mulgass2  20212  lss1d  20884  nzerooringczr  21405  cply1mul  22199  gsummoncoe1  22211  mp2pm2mplem4  22712  chpscmat  22745  chcoeffeq  22789  cnpnei  23167  hausnei2  23256  cmpsublem  23302  comppfsc  23435  filufint  23823  flimopn  23878  flimrest  23886  alexsubALTlem3  23952  equivcfil  25215  dvfsumrlim3  25956  pntlem3  27536  elntg2  28948  numedglnl  29107  cusgrsize2inds  29417  2pthnloop  29694  usgr2wlkneq  29719  elwspths2on  29923  clwwlkccatlem  29951  clwlkclwwlklem2a  29960  clwwisshclwws  29977  erclwwlktr  29984  erclwwlkntr  30033  3cyclfrgrrn1  30247  vdgn1frgrv2  30258  frgrncvvdeqlem8  30268  frgrwopreglem5  30283  frgrwopreglem5ALT  30284  frgr2wwlkeqm  30293  2clwwlk2clwwlk  30312  frgrregord013  30357  grpoinveu  30481  elspansn4  31535  atomli  32344  mdsymlem3  32367  mdsymlem5  32369  sat1el2xp  35354  satffunlem  35376  satffunlem1lem1  35377  satffunlem2lem1  35379  nn0prpwlem  36298  axc11n11r  36659  broucube  37636  rngoueqz  37922  rngonegrmul  37926  zerdivemp1x  37929  lshpdisj  38968  linepsubN  39734  pmapsub  39750  paddasslem5  39806  dalaw  39868  pclclN  39873  pclfinN  39882  trlval2  40145  tendospcanN  41005  diaintclN  41040  dibintclN  41149  dihintcl  41326  dvh4dimlem  41425  com3rgbi  44491  2reu8i  47101  ssfz12  47302  iccpartlt  47412  iccelpart  47421  iccpartnel  47426  fargshiftf1  47429  fargshiftfva  47431  sbcpr  47509  reuopreuprim  47514  lighneallem3  47595  lighneal  47599  sbgoldbwt  47765  grimcnv  47876  grimco  47877  isuspgrimlem  47883  uhgrimisgrgriclem  47918  grimedg  47923  cycl3grtri  47935  isubgr3stgrlem6  47959  grlicsym  48001  clnbgr3stgrgrlic  48008  pgnbgreunbgrlem3  48106  pgnbgreunbgrlem6  48112  lindslinindsimp1  48446