![]() |
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 1738 onint 7780 oalimcl 8562 oeordsuc 8596 fisup2g 9465 fiinf2g 9497 zorn2lem7 10499 inar1 10772 rpnnen1lem5 12967 expnbnd 14197 facwordi 14251 fi1uzind 14460 brfi1indALT 14463 unbenlem 16843 fiinopn 22410 cmpsublem 22910 dvcnvrelem1 25541 nocvxminlem 27286 axcontlem4 28263 axcont 28272 spansncol 30859 atcvat4i 31688 sumdmdlem 31709 broutsideof2 35169 relowlpssretop 36337 cvrat4 38406 pm2.43cbi 43367 |
Copyright terms: Public domain | W3C validator |