![]() |
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 1346 merco2 1731 onint 7793 oalimcl 8581 oeordsuc 8615 fisup2g 9492 fiinf2g 9524 zorn2lem7 10526 inar1 10799 rpnnen1lem5 12996 expnbnd 14227 facwordi 14281 fi1uzind 14491 brfi1indALT 14494 unbenlem 16877 fiinopn 22816 cmpsublem 23316 dvcnvrelem1 25963 nocvxminlem 27723 axcontlem4 28791 axcont 28800 spansncol 31391 atcvat4i 32220 sumdmdlem 32241 broutsideof2 35718 relowlpssretop 36843 cvrat4 38916 pm2.43cbi 43957 |
Copyright terms: Public domain | W3C validator |