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 7087 tfindsg 7569 tfr3 8029 pssnn 8730 dfac5 9548 cfcoflem 9688 isf32lem12 9780 ltexprlem7 10458 dirtr 17840 erclwwlktr 27794 erclwwlkntr 27844 3cyclfrgrrn1 28058 frgrregord013 28168 chirredlem1 30161 mdsymlem4 30177 cdj3lem2b 30208 ssfz12 43508 |
Copyright terms: Public domain | W3C validator |