![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > com4r | Structured version Visualization version GIF version |
Description: Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.) |
Ref | Expression |
---|---|
com4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
com4r | ⊢ (𝜃 → (𝜑 → (𝜓 → (𝜒 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | com4t 93 | . 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: com15 101 3expd 1415 elpwunsn 4452 onint 7275 tfindsg 7340 findsg 7373 tfrlem9 7766 tz7.49 7825 oaordi 7912 odi 7945 nnaordi 7984 nndi 7989 php 8434 fiint 8527 carduni 9142 dfac2b 9288 dfac2OLD 9290 axcclem 9616 zorn2lem6 9660 zorn2lem7 9661 grur1a 9978 mulcanpi 10059 ltexprlem7 10201 axpre-sup 10328 xrsupsslem 12453 xrinfmsslem 12454 supxrunb1 12465 supxrunb2 12466 mulgnnass 17965 fiinopn 21117 axcont 26329 sumdmdlem 29853 matunitlindflem1 34036 ee33VD 40058 |
Copyright terms: Public domain | W3C validator |