![]() |
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 7822 oalimcl 8612 oeordsuc 8646 fisup2g 9533 fiinf2g 9565 zorn2lem7 10567 inar1 10840 rpnnen1lem5 13042 expnbnd 14277 facwordi 14334 fi1uzind 14552 brfi1indALT 14555 unbenlem 16950 fiinopn 22921 cmpsublem 23421 dvcnvrelem1 26068 nocvxminlem 27831 axcontlem4 28991 axcont 29000 spansncol 31591 atcvat4i 32420 sumdmdlem 32441 broutsideof2 36078 relowlpssretop 37278 cvrat4 39348 pm2.43cbi 44429 |
Copyright terms: Public domain | W3C validator |