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

Theorem com15 99
Description: Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)
Hypothesis
Ref Expression
com5.1 (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏𝜂)))))
Assertion
Ref Expression
com15 (𝜏 → (𝜓 → (𝜒 → (𝜃 → (𝜑𝜂)))))

Proof of Theorem com15
StepHypRef Expression
1 com5.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏𝜂)))))
21com5l 98 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜏 → (𝜑𝜂)))))
32com4r 92 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:  injresinjlem  12450  addmodlteq  12607  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  swrdswrdlem  13311  2cshwcshw  13422  lcmfdvdsb  15194  initoeu1  16484  initoeu2lem1  16487  initoeu2  16489  termoeu1  16491  spthonepeq  26117  wlkdvspthlem  26137  erclwwlktr  26343  erclwwlkntr  26355  el2wlkonot  26396  3cyclfrgrarn1  26539  frgranbnb  26547  vdn0frgrav2  26550  frgrancvvdeqlemB  26565  usg2spot2nb  26592  numclwwlkovf2ex  26613  frgrareg  26644  frgraregord013  26645  zerdivemp1x  32916  bgoldbtbndlem4  40224  bgoldbtbnd  40225  tgoldbach  40232  tgoldbachOLD  40239  upgrwlkdvdelem  40942  spthonepeq-av  40958  usgr2pthlem  40969  erclwwlkstr  41243  erclwwlksntr  41255  3cyclfrgrrn1  41455  frgrnbnb  41463  frgrncvvdeqlemB  41477  av-numclwwlkovf2ex  41517  av-frgrareg  41548  av-frgraregord013  41549
  Copyright terms: Public domain W3C validator