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

Theorem com4t 93
Description: Commutation of antecedents. Rotate twice. (Contributed by NM, 25-Apr-1994.)
Hypothesis
Ref Expression
com4.1 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
Assertion
Ref Expression
com4t (𝜒 → (𝜃 → (𝜑 → (𝜓𝜏))))

Proof of Theorem com4t
StepHypRef Expression
1 com4.1 . . 3 (𝜑 → (𝜓 → (𝜒 → (𝜃𝜏))))
21com4l 92 . 2 (𝜓 → (𝜒 → (𝜃 → (𝜑𝜏))))
32com4l 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:  com4r  94  com24  95  isofrlem  6555  tfindsg  7022  tfr3  7455  pssnn  8138  dfac5  8911  cfcoflem  9054  isf32lem12  9146  ltexprlem7  9824  dirtr  17176  erclwwlkstr  26836  erclwwlksntr  26848  3cyclfrgrrn1  27047  frgrregord013  27141  chirredlem1  29137  mdsymlem4  29153  cdj3lem2b  29184  ssfz12  40651
  Copyright terms: Public domain W3C validator