![]() |
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 7360 tfindsg 7882 tfr3 8438 pssnn 9207 dfac5 10167 cfcoflem 10310 isf32lem12 10402 ltexprlem7 11080 dirtr 18660 erclwwlktr 30051 erclwwlkntr 30100 3cyclfrgrrn1 30314 frgrregord013 30424 chirredlem1 32419 mdsymlem4 32435 cdj3lem2b 32466 ssfz12 47264 |
Copyright terms: Public domain | W3C validator |