![]() |
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 1410 merco2 1780 onint 7273 oalimcl 7924 oeordsuc 7958 fisup2g 8662 fiinf2g 8694 zorn2lem7 9659 inar1 9932 rpnnen1lem5 12128 expnbnd 13312 facwordi 13394 fi1uzind 13593 brfi1indALT 13596 unbenlem 16016 fiinopn 21113 cmpsublem 21611 dvcnvrelem1 24217 axcontlem4 26316 axcont 26325 spansncol 28999 atcvat4i 29828 sumdmdlem 29849 nocvxminlem 32482 broutsideof2 32818 relowlpssretop 33807 cvrat4 35597 pm2.43cbi 39678 |
Copyright terms: Public domain | W3C validator |