| 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 2559 elpwunsn 4636 onint 7726 tfindsg 7794 findsg 7830 tfrlem9 8307 tz7.49 8367 oaordi 8464 odi 8497 nnaordi 8536 nndi 8541 php 9121 fiint 9216 fiintOLD 9217 carduni 9877 dfac2b 10025 axcclem 10351 zorn2lem6 10395 zorn2lem7 10396 grur1a 10713 mulcanpi 10794 ltexprlem7 10936 axpre-sup 11063 xrsupsslem 13209 xrinfmsslem 13210 supxrunb1 13221 supxrunb2 13222 mulgnnass 18988 fiinopn 22786 axcont 28925 sumdmdlem 32366 matunitlindflem1 37616 ee33VD 44872 |
| Copyright terms: Public domain | W3C validator |