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

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 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
com24 (𝜑 → (𝜃 → (𝜒 → (𝜓𝜏))))

Proof of Theorem com24
StepHypRef Expression
1 com4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21com4t 93 . 2 (𝜒 → (𝜃 → (𝜑 → (𝜓𝜏))))
32com13 88 1 (𝜑 → (𝜃 → (𝜒 → (𝜓𝜏))))
Colors of variables: wff setvar class
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  propeqop  5362  po2ne  5453  predpo  6134  fveqdmss  6823  tfrlem9  8004  omordi  8175  nnmordi  8240  fundmen  8566  pssnn  8720  fiint  8779  infssuni  8799  cfcoflem  9683  fin1a2lem10  9820  axdc3lem2  9862  zorn2lem7  9913  fpwwe2lem12  10052  genpnnp  10416  mulgt0sr  10516  nn01to3  12329  elfzodifsumelfzo  13098  ssfzo12  13125  elfznelfzo  13137  injresinjlem  13152  injresinj  13153  ssnn0fi  13348  expcan  13529  ltexp2  13530  hashgt12el2  13780  fi1uzind  13851  swrdswrdlem  14057  swrdswrd  14058  wrd2ind  14076  swrdccatin1  14078  cshwlen  14152  2cshwcshw  14178  cshwcsh2id  14181  dvdsmodexp  15607  dvdsaddre2b  15649  lcmfunsnlem2lem1  15972  lcmfdvdsb  15977  coprmproddvdslem  15996  infpnlem1  16236  cshwshashlem1  16421  initoeu1  17263  initoeu2lem1  17266  initoeu2  17268  termoeu1  17270  grpinveu  18130  mulgass2  19347  lss1d  19728  cply1mul  20923  gsummoncoe1  20933  mp2pm2mplem4  21414  chpscmat  21447  chcoeffeq  21491  cnpnei  21869  hausnei2  21958  cmpsublem  22004  comppfsc  22137  filufint  22525  flimopn  22580  flimrest  22588  alexsubALTlem3  22654  equivcfil  23903  dvfsumrlim3  24636  pntlem3  26193  elntg2  26779  numedglnl  26937  cusgrsize2inds  27243  2pthnloop  27520  usgr2wlkneq  27545  elwspths2on  27746  clwwlkccatlem  27774  clwlkclwwlklem2a  27783  clwwisshclwws  27800  erclwwlktr  27807  erclwwlkntr  27856  3cyclfrgrrn1  28070  vdgn1frgrv2  28081  frgrncvvdeqlem8  28091  frgrwopreglem5  28106  frgrwopreglem5ALT  28107  frgr2wwlkeqm  28116  2clwwlk2clwwlk  28135  frgrregord013  28180  grpoinveu  28302  elspansn4  29356  atomli  30165  mdsymlem3  30188  mdsymlem5  30190  sat1el2xp  32739  satffunlem  32761  satffunlem1lem1  32762  satffunlem2lem1  32764  nn0prpwlem  33783  axc11n11r  34130  broucube  35091  rngoueqz  35378  rngonegrmul  35382  zerdivemp1x  35385  lshpdisj  36283  linepsubN  37048  pmapsub  37064  paddasslem5  37120  dalaw  37182  pclclN  37187  pclfinN  37196  trlval2  37459  tendospcanN  38319  diaintclN  38354  dibintclN  38463  dihintcl  38640  dvh4dimlem  38739  com3rgbi  41218  2reu8i  43667  ssfz12  43869  iccpartlt  43939  iccelpart  43948  iccpartnel  43953  fargshiftf1  43956  fargshiftfva  43958  sbcpr  44036  reuopreuprim  44041  lighneallem3  44123  lighneal  44127  sbgoldbwt  44293  isomuspgrlem2b  44345  nzerooringczr  44694  lindslinindsimp1  44864
  Copyright terms: Public domain W3C validator