![]() |
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 1303 merco2 1701 onint 7037 oalimcl 7685 oeordsuc 7719 fisup2g 8415 fiinf2g 8447 zorn2lem7 9362 inar1 9635 rpnnen1lem5 11856 rpnnen1lem5OLD 11862 expnbnd 13033 facwordi 13116 fi1uzind 13317 brfi1indALT 13320 unbenlem 15659 fiinopn 20754 cmpsublem 21250 dvcnvrelem1 23825 axcontlem4 25892 axcont 25901 spansncol 28555 atcvat4i 29384 sumdmdlem 29405 nocvxminlem 32018 broutsideof2 32354 relowlpssretop 33342 cvrat4 35047 pm2.43cbi 39041 |
Copyright terms: Public domain | W3C validator |