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  imim12  105  propeqop  5100  predpo  5841  fveqdmss  6497  tfrlem9  7634  omordi  7800  nnmordi  7865  fundmen  8183  pssnn  8334  fiint  8393  infssuni  8413  cfcoflem  9296  fin1a2lem10  9433  axdc3lem2  9475  zorn2lem7  9526  fpwwe2lem12  9665  genpnnp  10029  mulgt0sr  10128  nn01to3  11984  elfzodifsumelfzo  12742  ssfzo12  12769  elfznelfzo  12781  injresinjlem  12796  injresinj  12797  ssnn0fi  12992  expcan  13120  ltexp2  13121  hashgt12el2  13413  fi1uzind  13481  swrdswrdlem  13668  swrdswrd  13669  wrd2ind  13686  swrdccatin1  13692  cshwlen  13754  2cshwcshw  13780  cshwcsh2id  13783  dvdsmodexp  15197  dvdsaddre2b  15238  lcmfunsnlem2lem1  15559  lcmfdvdsb  15564  coprmproddvdslem  15583  infpnlem1  15821  cshwshashlem1  16009  initoeu1  16868  initoeu2lem1  16871  initoeu2  16873  termoeu1  16875  grpinveu  17664  mulgass2  18809  lss1d  19176  cply1mul  19879  gsummoncoe1  19889  mp2pm2mplem4  20834  chpscmat  20867  chcoeffeq  20911  cnpnei  21289  hausnei2  21378  cmpsublem  21423  comppfsc  21556  filufint  21944  flimopn  21999  flimrest  22007  alexsubALTlem3  22073  equivcfil  23316  dvfsumrlim3  24016  pntlem3  25519  numedglnl  26261  cusgrsize2inds  26584  2pthnloop  26862  usgr2wlkneq  26887  elwspths2on  27108  clwwlkccatlem  27139  clwlkclwwlklem2a  27148  clwwisshclwws  27165  erclwwlktr  27172  erclwwlkntr  27229  clwlksfclwwlkOLD  27243  3cyclfrgrrn1  27467  vdgn1frgrv2  27478  frgrncvvdeqlem8  27488  frgrwopreglem5  27503  frgrwopreglem5ALT  27504  frgr2wwlkeqm  27513  2clwwlk2clwwlk  27534  frgrregord013  27594  grpoinveu  27713  elspansn4  28772  atomli  29581  mdsymlem3  29604  mdsymlem5  29606  nn0prpwlem  32654  axc11n11r  33010  broucube  33776  rngoueqz  34071  rngonegrmul  34075  zerdivemp1x  34078  lshpdisj  34796  linepsubN  35560  pmapsub  35576  paddasslem5  35632  dalaw  35694  pclclN  35699  pclfinN  35708  trlval2  35972  tendospcanN  36833  diaintclN  36868  dibintclN  36977  dihintcl  37154  dvh4dimlem  37253  com3rgbi  39245  ssfz12  41852  iccpartlt  41888  iccelpart  41897  iccpartnel  41902  fargshiftf1  41905  fargshiftfva  41907  lighneallem3  42052  lighneal  42056  sbgoldbwt  42193  nzerooringczr  42600  lindslinindsimp1  42774
  Copyright terms: Public domain W3C validator