![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > com4l | Structured version Visualization version GIF version |
Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Mel L. O'Cat, 15-Aug-2004.) |
Ref | Expression |
---|---|
com4.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
com4l | ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | com4.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | com3l 89 | . 2 ⊢ (𝜓 → (𝜒 → (𝜑 → (𝜃 → 𝜏)))) |
3 | 2 | com34 91 | 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: com4t 93 com4r 94 com14 96 com5l 100 3impd 1348 merco2 1734 onint 7828 oalimcl 8618 oeordsuc 8652 fisup2g 9539 fiinf2g 9571 zorn2lem7 10573 inar1 10846 rpnnen1lem5 13048 expnbnd 14283 facwordi 14340 fi1uzind 14558 brfi1indALT 14561 unbenlem 16957 fiinopn 22930 cmpsublem 23430 dvcnvrelem1 26078 nocvxminlem 27842 axcontlem4 29002 axcont 29011 spansncol 31602 atcvat4i 32431 sumdmdlem 32452 broutsideof2 36088 relowlpssretop 37332 cvrat4 39402 pm2.43cbi 44491 |
Copyright terms: Public domain | W3C validator |