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  5389  po2ne  5483  predpo  6160  fveqdmss  6839  tfrlem9  8012  omordi  8182  nnmordi  8247  fundmen  8572  pssnn  8725  fiint  8784  infssuni  8804  cfcoflem  9683  fin1a2lem10  9820  axdc3lem2  9862  zorn2lem7  9913  fpwwe2lem12  10052  genpnnp  10416  mulgt0sr  10516  nn01to3  12330  elfzodifsumelfzo  13093  ssfzo12  13120  elfznelfzo  13132  injresinjlem  13147  injresinj  13148  ssnn0fi  13343  expcan  13523  ltexp2  13524  hashgt12el2  13774  fi1uzind  13845  swrdswrdlem  14056  swrdswrd  14057  wrd2ind  14075  swrdccatin1  14077  cshwlen  14151  2cshwcshw  14177  cshwcsh2id  14180  dvdsmodexp  15605  dvdsaddre2b  15647  lcmfunsnlem2lem1  15972  lcmfdvdsb  15977  coprmproddvdslem  15996  infpnlem1  16236  cshwshashlem1  16419  initoeu1  17261  initoeu2lem1  17264  initoeu2  17266  termoeu1  17268  grpinveu  18078  mulgass2  19282  lss1d  19666  cply1mul  20392  gsummoncoe1  20402  mp2pm2mplem4  21347  chpscmat  21380  chcoeffeq  21424  cnpnei  21802  hausnei2  21891  cmpsublem  21937  comppfsc  22070  filufint  22458  flimopn  22513  flimrest  22521  alexsubALTlem3  22587  equivcfil  23831  dvfsumrlim3  24559  pntlem3  26113  elntg2  26699  numedglnl  26857  cusgrsize2inds  27163  2pthnloop  27440  usgr2wlkneq  27465  elwspths2on  27667  clwwlkccatlem  27695  clwlkclwwlklem2a  27704  clwwisshclwws  27721  erclwwlktr  27728  erclwwlkntr  27778  3cyclfrgrrn1  27992  vdgn1frgrv2  28003  frgrncvvdeqlem8  28013  frgrwopreglem5  28028  frgrwopreglem5ALT  28029  frgr2wwlkeqm  28038  2clwwlk2clwwlk  28057  frgrregord013  28102  grpoinveu  28224  elspansn4  29278  atomli  30087  mdsymlem3  30110  mdsymlem5  30112  sat1el2xp  32524  satffunlem  32546  satffunlem1lem1  32547  satffunlem2lem1  32549  nn0prpwlem  33568  axc11n11r  33915  broucube  34808  rngoueqz  35101  rngonegrmul  35105  zerdivemp1x  35108  lshpdisj  36005  linepsubN  36770  pmapsub  36786  paddasslem5  36842  dalaw  36904  pclclN  36909  pclfinN  36918  trlval2  37181  tendospcanN  38041  diaintclN  38076  dibintclN  38185  dihintcl  38362  dvh4dimlem  38461  com3rgbi  40728  2reu8i  43193  ssfz12  43395  iccpartlt  43431  iccelpart  43440  iccpartnel  43445  fargshiftf1  43448  fargshiftfva  43450  sbcpr  43530  reuopreuprim  43535  lighneallem3  43619  lighneal  43623  sbgoldbwt  43789  isomuspgrlem2b  43841  nzerooringczr  44241  lindslinindsimp1  44410
  Copyright terms: Public domain W3C validator