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

Theorem com24 81
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 79 . 2  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
32com13 74 1  |-  ( ph  ->  ( th  ->  ( ch  ->  ( ps  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com25  85  tfrlem5  6396  tfrlem9  6401  omordi  6564  nnmordi  6629  fundmen  6934  pssnn  7081  fiint  7133  cfcoflem  7898  fin1a2lem10  8035  axdc3lem2  8077  zorn2lem7  8129  fpwwe2lem12  8263  genpnnp  8629  mulgt0sr  8727  expcan  11154  ltexp2  11155  infpnlem1  12957  grpinveu  14516  mulgass2  15387  lss1d  15720  cnpnei  16993  hausnei2  17081  cmpsublem  17126  filufint  17615  flimopn  17670  flimrest  17678  alexsubALTlem3  17743  equivcfil  18725  dvfsumrlim3  19380  pntlem3  20758  grpoinveu  20889  rngoueqz  21097  elspansn4  22152  atomli  22962  mdsymlem3  22985  mdsymlem5  22987  predpo  24184  imgfldref2  25064  isunscov  25074  prl2  25169  oriso  25214  zerdivemp1  25436  svs2  25487  cmptdst  25568  limptlimpr2lem2  25575  bwt2  25592  hdrmp  25706  cmpmon  25815  cmpmor  25975  isibg1a6  26125  lppotos  26144  nn0prpwlem  26238  comppfsc  26307  rngonegrmul  26583  zerdivemp1x  26586  nbcusgra  28159  com3rgbi  28276  lshpdisj  29177  linepsubN  29941  pmapsub  29957  paddasslem5  30013  dalaw  30075  pclclN  30080  pclfinN  30089  trlval2  30352  tendospcanN  31213  diaintclN  31248  dibintclN  31357  dihintcl  31534  dvh4dimlem  31633
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator