Theorem com24 96

Description: Commutation of antecedents. Swap 2nd and 4th. Deduction associated with com13 89. (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 94	. 2 ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏))))
3	2	com13 89	1 ⊢ (𝜑 → (𝜃 → (𝜒 → (𝜓 → 𝜏))))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  com25  100  propeqop  5479  po2ne  5575  fveqdmss  7076  resf1extb  7944  tfrlem9  8386  omordi  8567  nnmordi  8633  fundmen  9052  pssnn  9177  fiint  9311  infssuni  9328  cfcoflem  10343  fin1a2lem10  10480  axdc3lem2  10522  zorn2lem7  10573  fpwwe2lem11  10719  genpnnp  11083  mulgt0sr  11183  nn01to3  13061  fzdif1  13732  elfzodifsumelfzo  13859  ssfzo12  13887  elfznelfzo  13901  injresinjlem  13918  injresinj  13919  ssnn0fi  14121  expcan  14305  ltexp2  14306  hashgt12el2  14561  fi1uzind  14645  swrdswrdlem  14846  swrdswrd  14847  wrd2ind  14865  swrdccatin1  14867  cshwlen  14943  2cshwcshw  14969  cshwcsh2id  14972  dvdsmodexp  16423  dvdsaddre2b  16470  lcmfunsnlem2lem1  16806  lcmfdvdsb  16811  coprmproddvdslem  16830  infpnlem1  17081  cshwshashlem1  17266  initoeu1  18179  initoeu2lem1  18182  initoeu2  18184  termoeu1  18186  grpinveu  19178  mulgass2  20533  lss1d  21231  nzerooringczr  21779  cply1mul  22607  gsummoncoe1  22619  mp2pm2mplem4  23120  chpscmat  23153  chcoeffeq  23197  cnpnei  23575  hausnei2  23664  cmpsublem  23710  comppfsc  23844  filufint  24232  flimopn  24287  flimrest  24295  alexsubALTlem3  24361  equivcfil  25613  dvfsumrlim3  26346  pntlem3  27929  elntg2  29556  numedglnl  29715  cusgrsize2inds  30027  2pthnloop  30310  usgr2wlkneq  30335  elwspths2on  30544  elwspths2onw  30545  clwwlkccatlem  30573  clwlkclwwlklem2a  30582  clwwisshclwws  30599  erclwwlktr  30606  erclwwlkntr  30655  3cyclfrgrrn1  30879  vdgn1frgrv2  30890  frgrncvvdeqlem8  30900  frgrwopreglem5  30915  frgrwopreglem5ALT  30916  frgr2wwlkeqm  30925  2clwwlk2clwwlk  30944  frgrregord013  30989  grpoinveu  31114  elspansn4  32168  atomli  32977  mdsymlem3  33000  mdsymlem5  33002  sat1el2xp  36123  satffunlem  36145  satffunlem1lem1  36146  satffunlem2lem1  36148  nn0prpwlem  37090  axc11n11r  37565  broucube  38552  rngoueqz  38854  rngonegrmul  38858  zerdivemp1x  38861  lshpdisj  40024  linepsubN  40789  pmapsub  40805  paddasslem5  40861  dalaw  40923  pclclN  40928  pclfinN  40937  trlval2  41200  tendospcanN  42060  diaintclN  42095  dibintclN  42204  dihintcl  42381  dvh4dimlem  42480  com3rgbi  45482  2reu8i  48152  ssfz12  48353  iccpartlt  48475  iccelpart  48484  iccpartnel  48489  fargshiftf1  48492  fargshiftfva  48494  sbcpr  48572  reuopreuprim  48577  lighneallem3  48661  lighneal  48665  sbgoldbwt  48844  grimcnv  48955  grimco  48956  isuspgrimlem  48962  uhgrimisgrgriclem  48997  grimedg  49002  cycl3grtri  49014  isubgr3stgrlem6  49038  grlicsym  49080  clnbgr3stgrgrlic  49087  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem6  49191  lindslinindsimp1  49538