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 7095 tfindsg 7577 tfr3 8037 pssnn 8738 dfac5 9556 cfcoflem 9696 isf32lem12 9788 ltexprlem7 10466 dirtr 17848 erclwwlktr 27802 erclwwlkntr 27852 3cyclfrgrrn1 28066 frgrregord013 28176 chirredlem1 30169 mdsymlem4 30185 cdj3lem2b 30216 ssfz12 43521 |
Copyright terms: Public domain | W3C validator |