Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > com4t | Structured version Visualization version GIF version |
Description: Commutation of antecedents. Rotate twice. (Contributed by NM, 25-Apr-1994.) |
Ref | Expression |
---|---|
com4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
com4t | ⊢ (𝜒 → (𝜃 → (𝜑 → (𝜓 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | com4l 92 | . 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏)))) |
3 | 2 | com4l 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 7127 tfindsg 7617 tfr3 8113 pssnn 8824 pssnnOLD 8872 dfac5 9707 cfcoflem 9851 isf32lem12 9943 ltexprlem7 10621 dirtr 18062 erclwwlktr 28059 erclwwlkntr 28108 3cyclfrgrrn1 28322 frgrregord013 28432 chirredlem1 30425 mdsymlem4 30441 cdj3lem2b 30472 ssfz12 44422 |
Copyright terms: Public domain | W3C validator |