![]() |
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 1350 mo4 2554 elpwunsn 4689 onint 7794 tfindsg 7866 findsg 7905 tfrlem9 8406 tz7.49 8466 oaordi 8567 odi 8600 nnaordi 8639 nndi 8644 php 9235 phpOLD 9247 fiint 9350 carduni 10006 dfac2b 10155 axcclem 10482 zorn2lem6 10526 zorn2lem7 10527 grur1a 10844 mulcanpi 10925 ltexprlem7 11067 axpre-sup 11194 xrsupsslem 13321 xrinfmsslem 13322 supxrunb1 13333 supxrunb2 13334 mulgnnass 19072 fiinopn 22847 axcont 28859 sumdmdlem 32300 matunitlindflem1 37220 ee33VD 44460 |
Copyright terms: Public domain | W3C validator |