MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com24 Unicode version

Theorem com24 83
Description: Commutation of antecedents. Swap 2nd and 4th. (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
StepHypRef Expression
1 com4.1 . . 3  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
21com4t 81 . 2  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
32com13 76 1  |-  ( ph  ->  ( th  ->  ( ch  ->  ( ps  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com25  87  tfrlem5  6600  tfrlem9  6605  omordi  6768  nnmordi  6833  fundmen  7139  pssnn  7286  fiint  7342  cfcoflem  8108  fin1a2lem10  8245  axdc3lem2  8287  zorn2lem7  8338  fpwwe2lem12  8472  genpnnp  8838  mulgt0sr  8936  elfznelfzo  11147  injresinjlem  11154  injresinj  11155  expcan  11387  ltexp2  11388  hashgt12el2  11638  brfi1uzind  11670  infpnlem1  13233  grpinveu  14794  mulgass2  15665  lss1d  15994  cnpnei  17282  hausnei2  17371  cmpsublem  17416  filufint  17905  flimopn  17960  flimrest  17968  alexsubALTlem3  18033  equivcfil  19205  dvfsumrlim3  19870  pntlem3  21256  nbcusgra  21425  cusgrasize2inds  21439  usgrasscusgra  21445  cyclnspth  21571  fargshiftf1  21577  fargshiftfva  21579  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  eupatrl  21643  grpoinveu  21763  rngoueqz  21971  zerdivemp1  21975  elspansn4  23028  atomli  23838  mdsymlem3  23861  mdsymlem5  23863  predpo  25398  nn0prpwlem  26215  comppfsc  26277  rngonegrmul  26458  zerdivemp1x  26461  ssfz12  27976  ssfzo12  27990  swrd0swrd  28009  swrdswrdlem  28010  swrdswrd  28011  swrdccatin1  28016  swrdccat3  28029  swrdccat3b  28031  usgra2pthspth  28035  el2wlkonot  28066  el2spthonot  28067  usg2wlkonot  28080  usg2wotspth  28081  frgraunss  28099  3cyclfrgrarn1  28116  3cyclfrgrarn  28117  vdfrgra0  28126  vdgfrgra0  28127  vdgn0frgrav2  28129  vdgn1frgrav2  28131  frgrancvvdeqlemB  28141  frgrawopreglem2  28148  frgrawopreglem5  28151  usg2spot2nb  28168  com3rgbi  28308  lshpdisj  29470  linepsubN  30234  pmapsub  30250  paddasslem5  30306  dalaw  30368  pclclN  30373  pclfinN  30382  trlval2  30645  tendospcanN  31506  diaintclN  31541  dibintclN  31650  dihintcl  31827  dvh4dimlem  31926
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator