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  4940  predpo  5667  fveqdmss  6320  tfrlem9  7441  omordi  7606  nnmordi  7671  fundmen  7990  pssnn  8138  fiint  8197  infssuni  8217  cfcoflem  9054  fin1a2lem10  9191  axdc3lem2  9233  zorn2lem7  9284  fpwwe2lem12  9423  genpnnp  9787  mulgt0sr  9886  nn01to3  11741  elfzodifsumelfzo  12490  ssfzo12  12518  elfznelfzo  12530  injresinjlem  12544  injresinj  12545  ssnn0fi  12740  expcan  12869  ltexp2  12870  hashgt12el2  13167  fi1uzind  13234  fi1uzindOLD  13240  swrdswrdlem  13413  swrdswrd  13414  wrd2ind  13431  swrdccatin1  13436  cshwlen  13498  2cshwcshw  13524  cshwcsh2id  13527  dvdsaddre2b  14972  lcmfunsnlem2lem1  15294  lcmfdvdsb  15299  coprmproddvdslem  15319  infpnlem1  15557  cshwshashlem1  15745  initoeu1  16601  initoeu2lem1  16604  initoeu2  16606  termoeu1  16608  grpinveu  17396  mulgass2  18541  lss1d  18903  cply1mul  19604  gsummoncoe1  19614  mp2pm2mplem4  20554  chpscmat  20587  chcoeffeq  20631  cnpnei  21008  hausnei2  21097  cmpsublem  21142  comppfsc  21275  filufint  21664  flimopn  21719  flimrest  21727  alexsubALTlem3  21793  equivcfil  23037  dvfsumrlim3  23734  pntlem3  25232  cusgrsize2inds  26270  2pthnloop  26530  usgr2wlkneq  26555  elwspths2on  26755  clwlkclwwlklem2a  26800  clwwisshclwws  26828  erclwwlkstr  26836  erclwwlksntr  26848  clwlksfclwwlk  26862  3cyclfrgrrn1  27047  vdgn1frgrv2  27058  frgrncvvdeqlemB  27069  frgrwopreglem5  27077  numclwwlkovf2ex  27109  frgrregord013  27141  grpoinveu  27261  elspansn4  28320  atomli  29129  mdsymlem3  29152  mdsymlem5  29154  nn0prpwlem  32012  axc11n11r  32368  broucube  33114  rngoueqz  33410  rngonegrmul  33414  zerdivemp1x  33417  lshpdisj  33793  linepsubN  34557  pmapsub  34573  paddasslem5  34629  dalaw  34691  pclclN  34696  pclfinN  34705  trlval2  34969  tendospcanN  35831  diaintclN  35866  dibintclN  35975  dihintcl  36152  dvh4dimlem  36251  com3rgbi  38241  ssfz12  40651  iccpartlt  40688  iccelpart  40697  iccpartnel  40702  fargshiftf1  40705  fargshiftfva  40707  lighneallem3  40853  lighneal  40857  bgoldbwt  40990  nzerooringczr  41390  lindslinindsimp1  41564
  Copyright terms: Public domain W3C validator