![]() |
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 1354 mo4 2561 elpwunsn 4645 onint 7726 tfindsg 7798 findsg 7837 tfrlem9 8332 tz7.49 8392 oaordi 8494 odi 8527 nnaordi 8566 nndi 8571 php 9157 phpOLD 9169 fiint 9271 carduni 9922 dfac2b 10071 axcclem 10398 zorn2lem6 10442 zorn2lem7 10443 grur1a 10760 mulcanpi 10841 ltexprlem7 10983 axpre-sup 11110 xrsupsslem 13232 xrinfmsslem 13233 supxrunb1 13244 supxrunb2 13245 mulgnnass 18916 fiinopn 22266 axcont 27967 sumdmdlem 31402 matunitlindflem1 36120 ee33VD 43249 |
Copyright terms: Public domain | W3C validator |