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  5508  po2ne  5605  fveqdmss  7081  tfrlem9  8385  omordi  8566  nnmordi  8631  fundmen  9031  pssnn  9168  pssnnOLD  9265  fiint  9324  infssuni  9343  cfcoflem  10267  fin1a2lem10  10404  axdc3lem2  10446  zorn2lem7  10497  fpwwe2lem11  10636  genpnnp  11000  mulgt0sr  11100  nn01to3  12925  elfzodifsumelfzo  13698  ssfzo12  13725  elfznelfzo  13737  injresinjlem  13752  injresinj  13753  ssnn0fi  13950  expcan  14134  ltexp2  14135  hashgt12el2  14383  fi1uzind  14458  swrdswrdlem  14654  swrdswrd  14655  wrd2ind  14673  swrdccatin1  14675  cshwlen  14749  2cshwcshw  14776  cshwcsh2id  14779  dvdsmodexp  16205  dvdsaddre2b  16250  lcmfunsnlem2lem1  16575  lcmfdvdsb  16580  coprmproddvdslem  16599  infpnlem1  16843  cshwshashlem1  17029  initoeu1  17961  initoeu2lem1  17964  initoeu2  17966  termoeu1  17968  grpinveu  18859  mulgass2  20121  lss1d  20574  cply1mul  21818  gsummoncoe1  21828  mp2pm2mplem4  22311  chpscmat  22344  chcoeffeq  22388  cnpnei  22768  hausnei2  22857  cmpsublem  22903  comppfsc  23036  filufint  23424  flimopn  23479  flimrest  23487  alexsubALTlem3  23553  equivcfil  24816  dvfsumrlim3  25550  pntlem3  27112  elntg2  28243  numedglnl  28404  cusgrsize2inds  28710  2pthnloop  28988  usgr2wlkneq  29013  elwspths2on  29214  clwwlkccatlem  29242  clwlkclwwlklem2a  29251  clwwisshclwws  29268  erclwwlktr  29275  erclwwlkntr  29324  3cyclfrgrrn1  29538  vdgn1frgrv2  29549  frgrncvvdeqlem8  29559  frgrwopreglem5  29574  frgrwopreglem5ALT  29575  frgr2wwlkeqm  29584  2clwwlk2clwwlk  29603  frgrregord013  29648  grpoinveu  29772  elspansn4  30826  atomli  31635  mdsymlem3  31658  mdsymlem5  31660  sat1el2xp  34370  satffunlem  34392  satffunlem1lem1  34393  satffunlem2lem1  34395  nn0prpwlem  35207  axc11n11r  35561  broucube  36522  rngoueqz  36808  rngonegrmul  36812  zerdivemp1x  36815  lshpdisj  37857  linepsubN  38623  pmapsub  38639  paddasslem5  38695  dalaw  38757  pclclN  38762  pclfinN  38771  trlval2  39034  tendospcanN  39894  diaintclN  39929  dibintclN  40038  dihintcl  40215  dvh4dimlem  40314  com3rgbi  43275  2reu8i  45821  ssfz12  46022  iccpartlt  46092  iccelpart  46101  iccpartnel  46106  fargshiftf1  46109  fargshiftfva  46111  sbcpr  46189  reuopreuprim  46194  lighneallem3  46275  lighneal  46279  sbgoldbwt  46445  isomuspgrlem2b  46497  nzerooringczr  46970  lindslinindsimp1  47138