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	|- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )

Assertion

Ref	Expression
com24	|- ( ph -> ( th -> ( ch -> ( ps -> ta ) ) ) )

Proof of Theorem com24

Step	Hyp	Ref	Expression
1		com4.1	. . 3 |- ( ph -> ( ps -> ( ch -> ( th -> ta ) ) ) )
2	1	com4t 93	. 2 |- ( ch -> ( th -> ( ph -> ( ps -> ta ) ) ) )
3	2	com13 88	1 |- ( ph -> ( th -> ( ch -> ( ps -> ta ) ) ) )

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  imim12  105  propeqop  4970  predpo  5698  fveqdmss  6354  tfrlem9  7481  omordi  7646  nnmordi  7711  fundmen  8030  pssnn  8178  fiint  8237  infssuni  8257  cfcoflem  9094  fin1a2lem10  9231  axdc3lem2  9273  zorn2lem7  9324  fpwwe2lem12  9463  genpnnp  9827  mulgt0sr  9926  nn01to3  11781  elfzodifsumelfzo  12533  ssfzo12  12561  elfznelfzo  12573  injresinjlem  12588  injresinj  12589  ssnn0fi  12784  expcan  12913  ltexp2  12914  hashgt12el2  13211  fi1uzind  13279  fi1uzindOLD  13285  swrdswrdlem  13459  swrdswrd  13460  wrd2ind  13477  swrdccatin1  13483  cshwlen  13545  2cshwcshw  13571  cshwcsh2id  13574  dvdsaddre2b  15029  lcmfunsnlem2lem1  15351  lcmfdvdsb  15356  coprmproddvdslem  15376  infpnlem1  15614  cshwshashlem1  15802  initoeu1  16661  initoeu2lem1  16664  initoeu2  16666  termoeu1  16668  grpinveu  17456  mulgass2  18601  lss1d  18963  cply1mul  19664  gsummoncoe1  19674  mp2pm2mplem4  20614  chpscmat  20647  chcoeffeq  20691  cnpnei  21068  hausnei2  21157  cmpsublem  21202  comppfsc  21335  filufint  21724  flimopn  21779  flimrest  21787  alexsubALTlem3  21853  equivcfil  23097  dvfsumrlim3  23796  pntlem3  25298  numedglnl  26039  cusgrsize2inds  26349  2pthnloop  26627  usgr2wlkneq  26652  elwspths2on  26853  clwlkclwwlklem2a  26899  clwwisshclwws  26928  erclwwlkstr  26936  erclwwlksntr  26948  clwlksfclwwlk  26962  3cyclfrgrrn1  27149  vdgn1frgrv2  27160  frgrncvvdeqlem8  27170  frgrwopreglem5  27185  frgrwopreglem5ALT  27186  frgr2wwlkeqm  27195  numclwwlkovf2exlem2  27212  frgrregord013  27253  grpoinveu  27373  elspansn4  28432  atomli  29241  mdsymlem3  29264  mdsymlem5  29266  nn0prpwlem  32317  axc11n11r  32673  broucube  33443  rngoueqz  33739  rngonegrmul  33743  zerdivemp1x  33746  lshpdisj  34274  linepsubN  35038  pmapsub  35054  paddasslem5  35110  dalaw  35172  pclclN  35177  pclfinN  35186  trlval2  35450  tendospcanN  36312  diaintclN  36347  dibintclN  36456  dihintcl  36633  dvh4dimlem  36732  com3rgbi  38720  ssfz12  41324  iccpartlt  41360  iccelpart  41369  iccpartnel  41374  fargshiftf1  41377  fargshiftfva  41379  lighneallem3  41524  lighneal  41528  sbgoldbwt  41665  nzerooringczr  42072  lindslinindsimp1  42246