|   | 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 7361 tfindsg 7883 tfr3 8440 pssnn 9209 dfac5 10170 cfcoflem 10313 isf32lem12 10405 ltexprlem7 11083 dirtr 18648 erclwwlktr 30042 erclwwlkntr 30091 3cyclfrgrrn1 30305 frgrregord013 30415 chirredlem1 32410 mdsymlem4 32426 cdj3lem2b 32457 relpfrlem 44979 ssfz12 47331 | 
| Copyright terms: Public domain | W3C validator |