![]() |
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 1352 mo4 2564 elpwunsn 4689 onint 7810 tfindsg 7882 findsg 7920 tfrlem9 8424 tz7.49 8484 oaordi 8583 odi 8616 nnaordi 8655 nndi 8660 php 9245 phpOLD 9257 fiint 9364 fiintOLD 9365 carduni 10019 dfac2b 10169 axcclem 10495 zorn2lem6 10539 zorn2lem7 10540 grur1a 10857 mulcanpi 10938 ltexprlem7 11080 axpre-sup 11207 xrsupsslem 13346 xrinfmsslem 13347 supxrunb1 13358 supxrunb2 13359 mulgnnass 19140 fiinopn 22923 axcont 29006 sumdmdlem 32447 matunitlindflem1 37603 ee33VD 44877 |
Copyright terms: Public domain | W3C validator |