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  6412  tfrlem9  6417  omordi  6580  nnmordi  6645  fundmen  6950  pssnn  7097  fiint  7149  cfcoflem  7914  fin1a2lem10  8051  axdc3lem2  8093  zorn2lem7  8145  fpwwe2lem12  8279  genpnnp  8645  mulgt0sr  8743  expcan  11170  ltexp2  11171  infpnlem1  12973  grpinveu  14532  mulgass2  15403  lss1d  15736  cnpnei  17009  hausnei2  17097  cmpsublem  17142  filufint  17631  flimopn  17686  flimrest  17694  alexsubALTlem3  17759  equivcfil  18741  dvfsumrlim3  19396  pntlem3  20774  grpoinveu  20905  rngoueqz  21113  elspansn4  22168  atomli  22978  mdsymlem3  23001  mdsymlem5  23003  predpo  24255  imgfldref2  25167  isunscov  25177  prl2  25272  oriso  25317  zerdivemp1  25539  svs2  25590  cmptdst  25671  limptlimpr2lem2  25678  bwt2  25695  hdrmp  25809  cmpmon  25918  cmpmor  26078  isibg1a6  26228  lppotos  26247  nn0prpwlem  26341  comppfsc  26410  rngonegrmul  26686  zerdivemp1x  26689  elfznelfzo  28213  injresinjlem  28214  injresinj  28215  hashgt12el2  28219  nbcusgra  28298  cyclnspth  28376  fargshiftf1  28382  fargshiftfva  28384  eupatrl  28385  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  3cyclfrgrarn1  28435  3cyclfrgrarn  28436  com3rgbi  28575  lshpdisj  29799  linepsubN  30563  pmapsub  30579  paddasslem5  30635  dalaw  30697  pclclN  30702  pclfinN  30711  trlval2  30974  tendospcanN  31835  diaintclN  31870  dibintclN  31979  dihintcl  32156  dvh4dimlem  32255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator