![]() |
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 1349 merco2 1739 onint 7778 oalimcl 8560 oeordsuc 8594 fisup2g 9463 fiinf2g 9495 zorn2lem7 10497 inar1 10770 rpnnen1lem5 12965 expnbnd 14195 facwordi 14249 fi1uzind 14458 brfi1indALT 14461 unbenlem 16841 fiinopn 22403 cmpsublem 22903 dvcnvrelem1 25534 nocvxminlem 27279 axcontlem4 28225 axcont 28234 spansncol 30821 atcvat4i 31650 sumdmdlem 31671 broutsideof2 35094 relowlpssretop 36245 cvrat4 38314 pm2.43cbi 43279 |
Copyright terms: Public domain | W3C validator |