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

Theorem com24 84
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 82 . 2  |-  ( ch 
->  ( th  ->  ( ph  ->  ( ps  ->  ta ) ) ) )
32com13 77 1  |-  ( ph  ->  ( th  ->  ( ch  ->  ( ps  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  com25  88  tfrlem5  6642  tfrlem9  6647  omordi  6810  nnmordi  6875  fundmen  7181  pssnn  7328  fiint  7384  infssuni  7398  cfcoflem  8153  fin1a2lem10  8290  axdc3lem2  8332  zorn2lem7  8383  fpwwe2lem12  8517  genpnnp  8883  mulgt0sr  8981  elfznelfzo  11193  injresinjlem  11200  injresinj  11201  expcan  11433  ltexp2  11434  hashgt12el2  11684  brfi1uzind  11716  infpnlem1  13279  grpinveu  14840  mulgass2  15711  lss1d  16040  cnpnei  17329  hausnei2  17418  cmpsublem  17463  bwth  17474  filufint  17953  flimopn  18008  flimrest  18016  alexsubALTlem3  18081  equivcfil  19253  dvfsumrlim3  19918  pntlem3  21304  nbcusgra  21473  cusgrasize2inds  21487  usgrasscusgra  21493  cyclnspth  21619  fargshiftf1  21625  fargshiftfva  21627  3v3e3cycl1  21632  4cycl4v4e  21654  4cycl4dv4e  21656  eupatrl  21691  grpoinveu  21811  rngoueqz  22019  zerdivemp1  22023  elspansn4  23076  atomli  23886  mdsymlem3  23909  mdsymlem5  23911  predpo  25460  nn0prpwlem  26326  comppfsc  26388  rngonegrmul  26569  zerdivemp1x  26572  ssfz12  28105  ssfzo12  28131  swrd0swrd  28198  swrdswrdlem  28199  swrdswrd  28200  swrdccatin1  28206  2cshwmod  28258  usgra2pthspth  28306  el2wlkonot  28337  el2spthonot  28338  usg2wlkonot  28351  usg2wotspth  28352  frgraunss  28386  3cyclfrgrarn1  28403  3cyclfrgrarn  28404  vdfrgra0  28413  vdgfrgra0  28414  vdgn0frgrav2  28416  vdgn1frgrav2  28418  frgrancvvdeqlemB  28428  frgrawopreglem2  28435  frgrawopreglem5  28438  usg2spot2nb  28455  com3rgbi  28598  lshpdisj  29786  linepsubN  30550  pmapsub  30566  paddasslem5  30622  dalaw  30684  pclclN  30689  pclfinN  30698  trlval2  30961  tendospcanN  31822  diaintclN  31857  dibintclN  31966  dihintcl  32143  dvh4dimlem  32242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator