| 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 2566 elpwunsn 4684 onint 7810 tfindsg 7882 findsg 7919 tfrlem9 8425 tz7.49 8485 oaordi 8584 odi 8617 nnaordi 8656 nndi 8661 php 9247 phpOLD 9259 fiint 9366 fiintOLD 9367 carduni 10021 dfac2b 10171 axcclem 10497 zorn2lem6 10541 zorn2lem7 10542 grur1a 10859 mulcanpi 10940 ltexprlem7 11082 axpre-sup 11209 xrsupsslem 13349 xrinfmsslem 13350 supxrunb1 13361 supxrunb2 13362 mulgnnass 19127 fiinopn 22907 axcont 28991 sumdmdlem 32437 matunitlindflem1 37623 ee33VD 44899 |
| Copyright terms: Public domain | W3C validator |